[CuriousCosmic]

I think the big issue is using tools without verification infrastructure. Of course there are specification level bugs to deal with but hacks seem to be oh so often the simple "I forgot to initialise a variable" kind of attacks.

I think we really need to be splitting up code for smart contracts into 3 classes:

- Low Complexity, Automated Assurance: Non-turing complete DSLs that allow you to fully reason about their behaviour and catch bugs in a near completely automated manner. The only one of these that I know of at the moment is Marlowe however I'd love to know if more existed. This class should be easily accessible by finance people and should be near impossible to get wrong.

- Medium Complexity, Semi-automated Assurance: These are tools that are expressive and more code than contract however they may or may not be turing complete. These can catch a wide number of bug classes but may need manual intervention (annotations or proofs) to cover the last mile.

- High Complexity, Manual Assurance: The are tools that give you the full power of a turing complete language and all the landmines that come with them. I personally believe any smart contract written with one of these tools should not be used in production unless it is accompanied with a formal specification and an end to end set of proofs verifying correctness.

At least with this model you can judge the risk factor by how complex your application is. 90% of smart contracts probably fall into the first class and another 9% probably fall into the second. There really is no reason to be using a tool without any reasonable amount of assurances provided unless your project is extraordinarily complex (and even then it'd probably cost a fortune to run on a network) and even then there's no reason for these smart contracts to exist without any proofs backing them.

[Paradigma11]

There are some interesting projects on Tezos in this regard:

https://archetype-lang.org/ is a non-turing complete dsl that you can run http://why3.lri.fr/ proofs on.

Another way is to run proofs on the michelson that was generated by a higher level language (https://ligolang.org/, https://hackage.haskell.org/package/morley ...) with: https://gitlab.com/nomadic-labs/mi-cho-coq

The most interesting project (still alpha i think) to me is: https://juvix.org/ a rather elegant dependently typed language.

[CuriousCosmic]

Thanks for those. I really like the work that Tezos has been doing and the more I see from them the more impressed I am.

By the way what's your thought on Plutus (https://developers.cardano.org/en/programming-languages/plut...)?

It's technically its own language however it is basically a Haskell DSL/library that lifts code into a smart contract domain. It seems to retain the full expressivity and safety of Haskell (and the Haskell tooling). Additionally it allows you to share the same code base for on and off network code (as the smart contract code is largely just code lifted into a smart contract domain. This provides pretty much seamless interaction between the two domains. The documentation is a bit sparse at the moment which is its biggest weakness however that's rapidly being improved with the approach of Alonzo at the end of July/start of August.

I'm honestly so glad we as a space are finally starting to move away from Solidity and all of its footguns.