[rust-dev] Ideas for academic/research work related to Rust and formal verification

Tim Chevalier catamorphism at gmail.com
Thu Oct 24 17:31:29 PDT 2013


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
<ilmars.cirulis at gmail.com> 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
> Rust-dev at mozilla.org
> 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


More information about the Rust-dev mailing list