4 ms·

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

by lmkg 13y ago

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.

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 ago
  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.
  - pavpanchekha 13y ago
    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.
kibwen 13y ago
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 https://github.com/nikomatsakis/rust-redex

by lmkg 13y ago

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 ago
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.
- pavpanchekha 13y ago
  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.

kibwen 13y ago

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 https://github.com/nikomatsakis/rust-redex