I am a fun of the inherently formally verified languages like haskell (used in
Cardano), or OCaml (used in
Tezos). Formally verified languages are secure languages, because their behavior is proved mathematically.
I am afraid of the intervention of the agents who want to control everything and especially the cryptocurrencies. Thats why we should rely on mathematical proof of the security of an algorithm or of a language, rather than rely on the skill or on the honesty of the developers, and this applies to Linus Torvalds too.
But of course , as a compromise, I could accept that rust or C are also fairly secure enviroments, unless it is proven otherwise.
Rust's first compiler that was used to create rust and compile the rest rust versions, was written in OCaml, then OCaml was abandonded and LLVM was used. I suspect that the agents may discovered a bug in this first OCaml version (or in the LLVM version) of Rust, that is inherited to all the rest rust versions and they want to get profit of it. Thats why they fired many old rust developers, and hired new ones that are under their control. This is of course a filthy conspiracy theory, and in order to be proved wrong we have to find the first version of rust written in OCaml, formally verify it, then create again the bootstrap of Rust and use it in order to compile the current rust version.
Getting started with Formal Verification Part 1: Introduction and Solvers - YouTube
A formally verified/secure software (or hardware) should be deterministic, or at least
a deterministic tree of states should spawn from a non-deterministic state. Polkadot devs believed that rust was secure, but after discovering a hidden non deterministic function they may changed their mind. Of course they are tighten to rust language now, and they cannot step back.
Lets not do their mistake, here in Dash. Lets formaly verify everything, lets be based on deterministic/secure/inherently formally verified languages.
Cardano did that, with haskell, and it is on top of coinmarketcap now.