Hi, Ilmārs -- One of the things we're hoping to do is a type safety proof for a subset of Rust. Because machine-checked proofs are so labor-intensive (and it's almost impossible to appreciate just how labor-intensive until you try a proof for an even slightly realistic language), the usual approach is to start with a proof for a pared-down subset of your subject language. It would be a very good idea to start with a core language that isolated only *one* feature, and removed everything else that isn't relevant to formalizing that feature. For example, with Rust, one place to start is a language with integers and owned pointers (no borrowed or managed pointers) as the only types.
To prove type soundness, you define an operational semantics for the sub-language you're working with, as well as a type system (static semantics) for it, and then prove that the two relate to each other (the usual reference on the basic approach is Benjamin Pierce's _Types and Programming Languages_, and Pierce's online book _Software Foundations_ shows how the proofs work in Coq). Again, if you did this for Rust, you'd want to start with the simplest possible subset of the language. https://github.com/mozilla/rust/issues/9883 is the issue tracking this task. Keep in mind that in that issue, we're thinking of a manual proof, not a machine-checked proof. We don't consider a machine-checked proof crucial for the success of the project, but it would certainly be an interesting project for somebody to undertake. The key to success is to limit the scope of the project severely, at least to start with. Niko Matsakis, on the core Rust team, has done some work already along these lines (formalization and manual proof, rather than machine-checked proof). I'm not sure how much of it is available. Cheers, Tim On Thu, Oct 24, 2013 at 5:25 PM, Ilmārs Cīrulis <[email protected]> wrote: > Greetings! > > (I hope this isn't spam.) > > I am bachelor's degree student (the first of four years) in Computer > Sciences. I am searching for any ideas that can be used as a research topic > and is both related to Rust and formal verification/specification or > similar. > I'm learning Coq already, so it's my choice for any formal stuff. > > Some of my random ideas (most of them possible maybe in some future, but not > now with rapidly development of Rust language): > * Formal specification of Rust (maybe similar to LambdaJS) - to use it later > in formal verification of Rust programs > * Program extraction from proof. This idea got its inspiration from > similarity of OCaml and Rust, and the fact that Coq allows extraction to > OCaml. > > I understand that my ideas most probably are the unrealistic ones, because I > have little to nothing experience and don't know what's is practical or even > what's topical in formal method academic research. Maybe you have some ideas > or suggestions? > I plan to use that for activities besides lectures and later for my bachelor > work. But then it's nice if it's something that academics/professors sees as > something meaningful. > > Anyway, thanks! > > > --- > Ilmārs Cīrulis > > _______________________________________________ > Rust-dev mailing list > [email protected] > https://mail.mozilla.org/listinfo/rust-dev > -- Tim Chevalier * http://catamorphism.org/ * Often in error, never in doubt "Being queer is not about a right to privacy; it is about the freedom to be public, to just be who we are." -- anonymous, June 1990 _______________________________________________ Rust-dev mailing list [email protected] https://mail.mozilla.org/listinfo/rust-dev
