undefined | Better HN

0 pointsekidd8y ago0 comments

Corecursion and codata are cool, and I would trust Solidity vastly more if it were a "total" functional language with no mutable state and aggressive type checking. Or if it were something more like https://www.idris-lang.org/ , where I had abundant tools to rigorously prove that nobody could steal my money.

Basically, if I'm going to spend even 5 minutes playing with smart contracts, I want to feel like the language designers were incredibly paranoid and aware of just how good modern languages can be at provability and security.

0 comments

4 comments · 1 top-level

mbrock8y ago· 3 in thread

If you're competent with proofs in Idris, you can write your EVM programs as an Idris DSL.

But, I mean, there's no proof that the Idris compiler does what it's supposed to do, so you'd still have a huge trusted base.

ekiddOP8y ago

> If you're competent with proofs in Idris, you can write your EVM programs as an Idris DSL.

Yeah, all my formal proof experience is with Coq, which is just a bit too idiosyncratic and difficult for this sort of thing. But I seem to remember that—especially if you're willing to certify specific results, and not necessarily the program in general—you can make your trusted computing base very small indeed.

I mean, if the CompCert C compiler can be as thoroughly verified as it is (http://compcert.inria.fr/compcert-C.html), there's no reason why it shouldn't be possible to verify smart contracts.

mbrock8y ago

Some pointers you might appreciate:

Jack Petterson and Robert Edström did a master's thesis about retargeting the Idris compiler to emit EVM code, with a custom effect type to express smart contract effects. They ended up modestly skeptical of functional programming as a paradigm for EVM, instead looking toward process calculi. https://publications.lib.chalmers.se/records/fulltext/234939...

Yoichi Hirai's summary of his research into Ethereum formal verification as a full-time formal methods researcher at the Foundation: https://github.com/pirapira/ethereum-formal-verification-ove...

See especially his formalization of the EVM as Hoare triples in Lem, which is usable from Isabelle: https://github.com/pirapira/eth-isabelle -- very cool stuff, although I have to say that the ostensible complexity and difficulty of his proof verifying an utterly simple wallet contract makes me a bit skeptical of this approach to smart contract correctness: https://github.com/pirapira/eth-isabelle/blob/master/example...

seanwilson8y ago

> I mean, if the CompCert C compiler can be as thoroughly verified as it is (http://compcert.inria.fr/compcert-C.html), there's no reason why it shouldn't be possible to verify smart contracts.

Hmm, so from the smart contract examples I've seen, I would have thought writing them in something like Coq would be quite feasible. The code examples I've seen tend to only have simple loops if any, basic conditions and the code is short (e.g. compared to something like web development or mobile apps). Writing anything inside a theorem prover is very challenging though but it seems a compelling application.

If you were implementing a smart contract in something like Coq, I'd be interested to read about what kind of specifications you would typically want to verify. I guess properties like "the owner of this wallet cannot be changed" and "the owner of this wallet can only accept money but not give it away" would be good ones.

j / k navigate · click thread line to collapse