They probably should've started with a Wirth-style language plus Design-by-Contract and static analysis. That would knock out tons of stuff at compile and runtime. If looking for mature language, the best one for predictability is SPARK Ada hands down. It was designed for easy analysis in automated provers. It's automation level is a lot higher than it used to be. Folks wanting provable programs should either be considering using it or prototyping their programs in it with semantics-preserving translation to the blockchain language/VM.

https://en.wikipedia.org/wiki/SPARK_(programming_language)

https://www.amazon.com/Building-High-Integrity-Applications-...

Note: The book is designed for people without formal methods background. I can't say how easy or not it will be since I just got it. :)

Are we there yet? 20 Years of Industrial Theorem Proving with SPARK

https://proteancode.com/keynote.pdf

IRONSIDES DNS illustrates it can handle bigger problems

http://ironsides.martincarlisle.com

Frama-C and SPARK both build on Why3 platform with its intermediate language WhyML. Work built on any of these three can usually be ported to the others. So, I'll drop a recent example in Frama-C that's really math heavy with a style amenable to high automation.

https://hal.archives-ouvertes.fr/hal-01681134/document

Cobol has all of C's memory pitfalls, and a few extra. It can be truly painful.

A lot of dev's avoid dynamic allocation altogether, because of the issues you can face:

* Integer overflow

* Buffer overflow

* Free does not mean freed memory. It means freed memory at some point in the future.

If you want something safe, time-tested and performant for business logic, then something like Ada would be a better fit.

If you don't mind the safety problems, then just about nothing beats out FORTRAN in the numbers game. (Though the memory pitfalls are huge). It was one of COBOL's main competitors, and half of the world's banking infrastructure still runs on it.

Is it possible to implement a compiles to solidity or compiles to evm language with better properties? I assume yes.

Yea, Solidity is not the only language of code that compiles to EVM bytecode. There are other languages that also do so: Serpent, LLL, and Viper. "Better" is subjective, but it looks like Viper is intended to be more audit-able. But it's also still a work in progress.

Serpent and LLL are apparently lower-level than Solidity.

https://steemit.com/ethereum/@balzss/the-many-languages-of-e...

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

Serpent is deprecated.

It would (probably) be fairly trivial to get any modular compiler to spit out bytecode for the Etherium VM...fairly trivial for someone with the gumption and skills I mean.

Or someone could add some analysis stages to the solidity compiler since all the information you need is floating around the web in various papers -- actually spent a good part of the last week reading about abstracting abstract machines and static analysis for my next investigative coding project when I quit being lazy.

One of the Ethereum guys is working on a new smart contract language called Bamboo that looks pretty interesting.

Why not Rust or Haskell?