3 ms·
Few languages have any formal verification work at all. There is a verified C compiler (CompCert; it comes with a guarantee that the compiled assembly is a corr
by pavpanchekha 13y ago
Few languages have any formal verification work at all. There is a verified C compiler (CompCert; it comes with a guarantee that the compiled assembly is a correct compilation of the source, and it does some very basic verified optimizations) and a verified ML compiler (CakeML, see this year's POPL proceedings).
Few languages have verified anything—verification is still very challenging to do.
- mccr8 13y agoA proof of type safety of a language, which I think is what pcwalton is talking about, is a different beast than the proof of the correctness of a compiler, which is what you are talking about.
- pavpanchekha 13y agoI actually cannot think of any languages except SML that have complete formal proofs of type safety. Now, I may simply be forgetting something obvious. But Haskell's type systems keeps growing by little features here and there, so no full proof is anywhere; OCaml doesn't have a formal semantics, so it sure as hell doesn't have a proof of type safety (in the usual "a well-typed program doesn't go wrong" sense); Java is unsound (in a particular manner of speaking, of course); C# seems too complicated to have such a proof. The Go authors don't seem the type. Rust is the language in question. Those seem like the big players.