“A good smart contract language is a $1 billion problem. Why? Look at the amounts lost in some recent hacks:”
Why aren’t more of them just trying SPARK Ada if it’s so costly to fail and they need a language? I’ve never understood this. Let’s say it’s $3000 a license. That’s probably high but on purpose. They’re pulling in millions to a billion dollars. Any coding errors can loose that. SPARK gets them immunity to most coding errors plus easier proof of their contracts. Using a constrained, functional style makes that even easier. They get this assurance for a few grand. The increased use of SPARK for smart contracts makes AdaCore and CompSci start developing all kinds of libraries and theories that increase automation in those kind of works. Other projects outside SPARK, including FOSS, will follow suite to match it.
Don’t get me wrong: I find all this work really interesting. I even expect new stuff to be developed in parallel with using proven stuff. That the cryptocurrencies are also bringing mainstream audience into formal methods is neat, too, since how else is that going to happen [1]? ;) It’s just strange that most are avoiding tools proven to do the job to try prototype tools when there’s so much risk. At the least, I’d expect people to default on things like SPARK until alternatives mature and have many successes under their belt.
[1] Hopefully @hwayne’s TLA+ book if nothing else outside of cryptocurrencies. I’m really hoping and betting on that one given so many startups are doing distributed systems needing a way to bulletproof them faster and cheaper.
re your article
Your work on Pyramid looks really good. You made it small, useful, and have testing/model-checking by default. Probably all wise decisions given target audience. Presented in a clear, accessible way. Great stuff. :)
I especially liked that you tied it to Beautiful Racket. Reason is that I was looking at it just a few days ago when it got posted to Hacker News for similar purpose: a C-like language oriented toward verification and metaprogramming. Although putting the project off for months, I keep coming back to the idea of Racket tying the style to books like HtDP, SICP, and/or Beautiful Racket for onboarding new contributors more easily. They get to learn Scheme, metaprogramming, an IDE for both, and a step into highly-robust code in one, smooth flow. Whereas, outside of Racket or done in separate languages, the higher barrier to entry might force them to learn less since they have to pick and choose.
So, the language gets Racket’s tooling/IDE, it’s easier to build, they get benefit of learning Racket, and they get to learn the verification-oriented language in it. What you think on those potential advantages of Racket for high-assurance languages? It looks like you’re doing something similar but you might have some other reasons.
One problem there is that Ethereum has a custom instruction set, so no existing languages can compile to it. That leaves Solidity as the only option.
Cardano are using a formally-specified variant of LLVM. Since there is an Ada for LLVM, it should be possible to use Ada to program Cardano contracts when they release it in the next few weeks.
Some Ethereum people want to use WebAssembly for the next version of its VM. People mainly interact with Ethereum applications via websites and the Metamask browser extension, so this lets them share code between their websites and the contracts. I’m skeptical myself.
Ethereum contracts are vulnerable to a different class of bugs than ordinary software, so most people’s suggestions for “improving” security are targeting the wrong issues. I see that SPARK purports to support bounds on space and time. That actually makes it far better than most suggestions, since this is a crucial security requirement in Ethereum.
For example, the DAO issue was a “re-entrancy” attack, where the same contract is run multiple times within the same transaction. Protecting against this requires all state-modifying code to be idempotent.
I like your idea of writing a high-assurance language in Racket. I’m considering picking up the PLT Redex book[1] myself. Writing my C compiler has made me think that every standardized language should have a formal semantics:
C:
int x = sizeof(x++);
Lisp IR:
(define x (allocate-local *platform-native-size*))
(write-local x (type-size (expression-type (+ x 1))))
The C++ standard would be much shorter if it came with a precise Lisp dialect. And a verification language seems like it needs a clear semantics to know what exactly it’s verifying.
Yeah, SPARK was meant for real-time applications with space and memory bounds. So, I figured there should be overlap in what it does and Ethereum needs. Good news on Cardano having a potential tie-in to Ada via LLVM.
Far as using SPARK, I knew the EVM used its own instruction set. My concept was more modeling those operations in SPARK similar to how many have done with typed x86 or abstract machines. You essentially make a state machine for EVM in SPARK that lets you verify EVM assebly. Then, you model your contract in high-level SPARK that’s close to the machine. After proving those properties, you do a hand- or tool-based translation to EVM modeled in SPARK. If the contract is simple, then the assembly equivalence might be straight-forward to check by eye (caveat: I don’t know EVM). Reduces need for trusted compiler. The properties of the contract are then proven on the simulated assembly in SPARK. That’s extracted by hand or tool into actual EVM again checked by eye since they should look about the same.
You’re actually stronger in formal verification than me since you actually do it vs read about it. Haha. So, I’m curious how effective you think that might be. There’s prior art but each project is different. Outside SPARK, the TALC and X86.Proved projects give me hope these simpler assemblies could be tackled with approachable tooling.
re Racket
Yeah, I agree on semantics formally or in LISP for new languages. It’s a good check on complexity. Btw, one of the works I plan to draw on is ZL which essentially is C++ in Scheme. I imagine the two people it took to do that with C compatibility was less work than it would take (did take) to do it in C or C++ themselves. I’m just speculating as a guy who has seen productivity studies on LISP vs C/C++… ;)
PLT Redex looks good. Thanks for the tip. Bookmarking it. Far as blockchain VM’s, one more work that you’ve probably seen but just giving it to you in case you haven’t. It’s about a newer one while also referencing their EVM work. Rosu’s group seem to be the most productive on formally specifying languages that, via their K Framework, automatically get some useful tooling. That C Semantics is still jaw dropping work to me given how many barely-functional attempts I’ve read over the years at modeling things like mini-Pascals or partial versions of C. They usually had no tooling, too. Building these languages on Racket, K Framework, or preferably both is a substantial improvement to where high-assurance languages were at just five years ago.
WebAssembly is just a well-specified VM to do computation. I too am skeptical about code sharing argument, but it seems to me WebAssembly is clearly superior to LLVM, which was designed as a compiler IR and very much not designed as a portable assembly. What’s your main problems with WebAssembly?
re related topic
“A good smart contract language is a $1 billion problem. Why? Look at the amounts lost in some recent hacks:”
Why aren’t more of them just trying SPARK Ada if it’s so costly to fail and they need a language? I’ve never understood this. Let’s say it’s $3000 a license. That’s probably high but on purpose. They’re pulling in millions to a billion dollars. Any coding errors can loose that. SPARK gets them immunity to most coding errors plus easier proof of their contracts. Using a constrained, functional style makes that even easier. They get this assurance for a few grand. The increased use of SPARK for smart contracts makes AdaCore and CompSci start developing all kinds of libraries and theories that increase automation in those kind of works. Other projects outside SPARK, including FOSS, will follow suite to match it.
Don’t get me wrong: I find all this work really interesting. I even expect new stuff to be developed in parallel with using proven stuff. That the cryptocurrencies are also bringing mainstream audience into formal methods is neat, too, since how else is that going to happen [1]? ;) It’s just strange that most are avoiding tools proven to do the job to try prototype tools when there’s so much risk. At the least, I’d expect people to default on things like SPARK until alternatives mature and have many successes under their belt.
[1] Hopefully @hwayne’s TLA+ book if nothing else outside of cryptocurrencies. I’m really hoping and betting on that one given so many startups are doing distributed systems needing a way to bulletproof them faster and cheaper.
re your article
Your work on Pyramid looks really good. You made it small, useful, and have testing/model-checking by default. Probably all wise decisions given target audience. Presented in a clear, accessible way. Great stuff. :)
I especially liked that you tied it to Beautiful Racket. Reason is that I was looking at it just a few days ago when it got posted to Hacker News for similar purpose: a C-like language oriented toward verification and metaprogramming. Although putting the project off for months, I keep coming back to the idea of Racket tying the style to books like HtDP, SICP, and/or Beautiful Racket for onboarding new contributors more easily. They get to learn Scheme, metaprogramming, an IDE for both, and a step into highly-robust code in one, smooth flow. Whereas, outside of Racket or done in separate languages, the higher barrier to entry might force them to learn less since they have to pick and choose.
So, the language gets Racket’s tooling/IDE, it’s easier to build, they get benefit of learning Racket, and they get to learn the verification-oriented language in it. What you think on those potential advantages of Racket for high-assurance languages? It looks like you’re doing something similar but you might have some other reasons.
Thanks for reading, Nick.
One problem there is that Ethereum has a custom instruction set, so no existing languages can compile to it. That leaves Solidity as the only option.
Cardano are using a formally-specified variant of LLVM. Since there is an Ada for LLVM, it should be possible to use Ada to program Cardano contracts when they release it in the next few weeks.
Some Ethereum people want to use WebAssembly for the next version of its VM. People mainly interact with Ethereum applications via websites and the Metamask browser extension, so this lets them share code between their websites and the contracts. I’m skeptical myself.
Ethereum contracts are vulnerable to a different class of bugs than ordinary software, so most people’s suggestions for “improving” security are targeting the wrong issues. I see that SPARK purports to support bounds on space and time. That actually makes it far better than most suggestions, since this is a crucial security requirement in Ethereum.
For example, the DAO issue was a “re-entrancy” attack, where the same contract is run multiple times within the same transaction. Protecting against this requires all state-modifying code to be idempotent.
I like your idea of writing a high-assurance language in Racket. I’m considering picking up the PLT Redex book[1] myself. Writing my C compiler has made me think that every standardized language should have a formal semantics:
C:
Lisp IR:
The C++ standard would be much shorter if it came with a precise Lisp dialect. And a verification language seems like it needs a clear semantics to know what exactly it’s verifying.
[1] https://mitpress.mit.edu/books/semantics-engineering-plt-redex
re SPARK/EVM
Yeah, SPARK was meant for real-time applications with space and memory bounds. So, I figured there should be overlap in what it does and Ethereum needs. Good news on Cardano having a potential tie-in to Ada via LLVM.
Far as using SPARK, I knew the EVM used its own instruction set. My concept was more modeling those operations in SPARK similar to how many have done with typed x86 or abstract machines. You essentially make a state machine for EVM in SPARK that lets you verify EVM assebly. Then, you model your contract in high-level SPARK that’s close to the machine. After proving those properties, you do a hand- or tool-based translation to EVM modeled in SPARK. If the contract is simple, then the assembly equivalence might be straight-forward to check by eye (caveat: I don’t know EVM). Reduces need for trusted compiler. The properties of the contract are then proven on the simulated assembly in SPARK. That’s extracted by hand or tool into actual EVM again checked by eye since they should look about the same.
You’re actually stronger in formal verification than me since you actually do it vs read about it. Haha. So, I’m curious how effective you think that might be. There’s prior art but each project is different. Outside SPARK, the TALC and X86.Proved projects give me hope these simpler assemblies could be tackled with approachable tooling.
re Racket
Yeah, I agree on semantics formally or in LISP for new languages. It’s a good check on complexity. Btw, one of the works I plan to draw on is ZL which essentially is C++ in Scheme. I imagine the two people it took to do that with C compatibility was less work than it would take (did take) to do it in C or C++ themselves. I’m just speculating as a guy who has seen productivity studies on LISP vs C/C++… ;)
PLT Redex looks good. Thanks for the tip. Bookmarking it. Far as blockchain VM’s, one more work that you’ve probably seen but just giving it to you in case you haven’t. It’s about a newer one while also referencing their EVM work. Rosu’s group seem to be the most productive on formally specifying languages that, via their K Framework, automatically get some useful tooling. That C Semantics is still jaw dropping work to me given how many barely-functional attempts I’ve read over the years at modeling things like mini-Pascals or partial versions of C. They usually had no tooling, too. Building these languages on Racket, K Framework, or preferably both is a substantial improvement to where high-assurance languages were at just five years ago.
WebAssembly is just a well-specified VM to do computation. I too am skeptical about code sharing argument, but it seems to me WebAssembly is clearly superior to LLVM, which was designed as a compiler IR and very much not designed as a portable assembly. What’s your main problems with WebAssembly?