Competition DeepSEA Blockchain - Glow-Lang/glow GitHub Wiki

DeepSEA/Blockchain is a general-purpose language for writing code at the level of abstraction of C, but with proofs of correctness using separation logic in Coq. You can do anything with it, including proving smart contract, but you're going to have to have a large team of PhD-level logicians do it the hard way; and then you'll have to separately prove your client and server code, and prove that they work together. The approach just doesn't scale. But maybe if someone actually uses it, they will build new abstractions on top of it, that are more usable.