It would be nice if everything were written in Coq or Isabelle with proof so that you could generate a correct program in a systems language from it. The proof

It would be nice if everything were written in Coq or Isabelle with proof so that you could generate a correct program in a systems language from it. The proof checker is much more ruthless than the rust compiler.