I'm looking forward to the Red[1] C3 project[2]. Red is a powerful language. I think they stand a chance to do some interesting things in the blockchain space.
Despite being based on semi-functional programming language Scala, I found no evidence that the language AxLang has anything to do with formal verification. I may be wrong, but what I see now is lots of promises without any details.
How do you mean? There are examples of formal verification working in the video. The resulting compiled smart contracts are on the live Ethereum blockchain.
Not related to Ethereum, but I've done some small prototyping of how smart contracts without side effects could be implemented in JavaScript and all compiling to it languages, even the pure functional ones https://github.com/slavasn/bloqly
Solidity as a language is not that bad. It wouldn't be my first choice but it wouldn't be my last.
Most of the challenges are not at the language level, they're at the EVM level. Any languages on top of the EVM are hamstrung by the EVMs limitations. If it were as easy as "just throw Rust/Go/Java on top of it", that would have already been done.
What do you see as the biggest flaws in the EVM as such?
I think a lot of the difficulty is that it's such a novel runtime environment, and it's going to take a few design/failure iterations to come up with a programming model which fits it.
The biggest flaw: EVM allows integer overflow. This has been responsible for many hacks. (aka somehow withdraw 1 token from 0 token account, now you have LOTS token!) I can't even imagine what they were thinking...
They may have changed it in recent versions, but for a long while, functions were public by default (i.e. anyone can call them). Defaulting to open is a huge security flaw and the reason behind the Parity bug https://blog.comae.io/the-280m-ethereums-bug-f28e5de43513
https://www.michaelburge.us/2017/11/28/write-your-next-ether...