bamboo

Bamboo looks quite interesting. I think it’s mainly focused on modelling the state changes smart contracts undergo more explicitly. https://github.com/pirapira/bamboo

Bamboo is a formally verifiable programming language being developed for Ethereum: https://github.com/pirapira/bamboo The Bamboo manifest: https://github.com/pirapira/bamboo/blob/master/doc/manifest.... There is a project under way to formalize Viper, which is the other newly developed programming language for Ethereum, as well: https://runtimeverification.com/blog/?p=411

Sure, but I'm not aware of any language with an optimizer that minimizes permanent storage (for example). The gas model has been forced to be a close representation of actual costs, because last year it wasn't close enough, and someone took advantage of that to launch denial of service attacks. Incidentally, last year someone wrote an Idris backend compiling to EVM for their doctoral thesis. They concluded that it had some benefits but not as much as they expected. [1] There's an effort in progress to migrate from the existing EVM to a modified webassembly [2], which would allow usage of existing languages, and potentially improve performance significantly. It's still experimental and may or may not work out, but seems to be making good progress. [3] With the existing EVM there are new languages in development that may improve matters, in

Worth mentioning that there is at least one other language being built on top of the EVM: https://github.com/pirapira/bamboo This one takes a strict state machine approach, and aims to solve some of the tricky reentry and state tracking problems of Solidity.

>Honest question, what would be required in your opinion for before we start considering if the tool is at fault? The programming language being partly at fault is not the same thing as it being "practically impossible" to write safe smart contracts that language, in my opinion. I was taking issue with your wording, which I think gives a misleading impression of the attainability of secure Solidity code. Your follow up comment is more measured, as it doesn't characterise the need for some measure of luck to write a safe smart contract as writing a secure smart contract being "practically impossible". Maybe we're using different definitions of "safe", but I think many use my definition, in which case your statement would give them a misleading impression. >This discussion is very similar to putting Ed25519 on the EVM. While you can technic

Ethereum developers use Solidity almost exclusively, because it is by far the most developed, but there is also Serpent, Viper and LLL. I don't know if Serpent and LLL are still being actively developed. Yoichi Hirai is also developing Bamboo [1]. [1] https://github.com/pirapira/bamboo