What is the current state of formal verification in Rust (of the language, of compilers, of other programs)? I would assume that since parts of the language are still undergoing change there isn't much work towards super-rigorous proofs until that gets nailed down. Has there been any provisional work in this direction, and is there any work towards making formal methods practical for Rust?
I like the idea of formal methods, but my familiarity with the subject is entry-level at best, so I don't even know what sort of details I should be asking about here =P.
Niko Matsakis, Rust's type theory guru, has been working on a formal model of Rust's type system to prove its soundness. Not sure how much of it is published yet, but I did find this: https://github.com/nikomatsakis/rust-redex
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.
A 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.
I 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.
I like the idea of formal methods, but my familiarity with the subject is entry-level at best, so I don't even know what sort of details I should be asking about here =P.