[lomnakkus]

It's a good indicator that these people may be experts in one area, but not necessarily in others.

Language design is actually notoriously difficult in general[1], but if you're doing language design for a security-critical language[2]... well, that requires actual mechanized proof, IMO. Not just proof of "design", but proof of the implementation. Anything else is a huge gamble. (And I'm sure there are some 'investors'/gamblers who made off very well.)

[1] Beyond surface-level, obviously.

[2] We're talking about 0.0001% of the general population here.

[buckie]

> Not just proof of "design", but proof of the implementation.

Absolutely, few people really get this. Even those that do get it generally don't know what it looks like in practice because it's so rare.

In case you're curious about what it looks like in practice (at least one way), we presented direct user code compilation and verification[1] in Jan for our smart contract language Pact[2].

The idea that you can write a doc test that triggers a formal verification about some aspect of your code is, for lack of a better term, strange and yet the power to weight ratio is just off the charts. For the first few days that the system started working (I built the FV portion, Stuart the language + H-M type system) I thought it was broken... turned out we just had a bug in our demo code that we never noticed.

Usually, tests check the things you know to check so when they find something it's not a surprise what they find. Sometimes you can fuzz and randomly find something, which is cool but doesn't guarantee that there isn't a problem somewhere else. However, FV just feels uncanny (as a dev) because the test either finds a problem in the code -- and tells you how to replicate the bug -- OR proves that a problem cannot exist.

[1]: https://youtu.be/Nw1glriQYP8?t=1071

[2]: kadena.io/pact

[lomnakkus]

> The idea that you can write a doc test that triggers a formal verification about some aspect of your code is, for lack of a better term, strange and yet the power to weight ratio is just off the charts.

I'm not sure I understand this sentence. Are you doing doctests, or are your doctests statements of formal properties, or have you abandoned that and are now doing formal specs->code type things?

[buckie]

It's closest to the middle, assuming that you meant that you're stating the properties that you want to test. It does more than that, but at its base that's effectively how it works so it's close enough for a solid intuition. We're working on a paper about it now -- or at least a sub-paper in the clutch of papers that pertain to a public chain version -- that I'll link to when it's out (a couple weeks probably).

[lomnakkus]

Oh. Dear?

(I mean, I understand the pressures of academia, but... ridiculously bad timing, yeah?)

[buckie]

Why bad timing? This is really just an example that while safe smart contracts are technically possible using Solidity/EVM, it's practically impossible. "One of the best Solidity devs" just failed to write a safe contract to the tune of a $30M exploit. Given that, what chance does anyone else have?

At some point, it's time to blame the tool and not the user. Moreover, it's not like people didn't see this coming, myself included[1]. I mean, who really thought that basically taking JavaScript and swapping out the DOM for a bank account wasn't going to end badly? But then again, maybe I've spent too much time at in the SEC/finance where "move fast and break things" engineering gets you shown the door quite quickly. That mantra's fine for a number of domains but finance isn't one of them as one bug can bankrupt the company (see: knight capital).

It really just underlines the need for a safer/better approach. Formal Verification has to be part of that story. A language that was designed with safety in mind has to be another part.

Also, not an academic (yet at least). Cofounder here: http://kadena.io

[1]: https://goldsilverbitcoin.com/jp-morgans-blockchain-research...

[Jabanga]

>This is really just an example that while safe smart contracts are technically possible using Solidity/EVM, it's practically impossible.

I don't see any justification for this statement. The bug could easily have been discovered if there had been better auditing. That the auditing missed the bug doesn't prove that it's "practically impossible" to write secure code with Solidity.

In any case, nothing is stopping you from porting your formally verifiable language to Ethereum. The EVM is not Solidity. In fact there is already a project underway to create a verifiable programming language for the EVM.

[goldfeld]

Experts in what area? Not in programming, to think exposing functionality by default is a good design concept.