3 ms·
This project uses one-way translation of Rust code into WhyML through Creusot. This translation is not formally guaranteed to be correct or semantics-preserving
by thesz 4y ago
This project uses one-way translation of Rust code into WhyML through Creusot. This translation is not formally guaranteed to be correct or semantics-preserving.
Ideally, the code produced by Creusot should be translated back to Rust by a tool from Creusot or someone else. This way it is possible to use fixed point iteration, just like AST pretty-printer and parser for programming language syntax.
This is more or less an approach taken by verification team of Buran (USSR's space shuttle) software. They took Fortran code and compiled it into executable code. The executable code was then manually translated back into Fortran and discrepancies analyzed. This way they found several errors in Fortran compiler. Buran made fully automatic landing in late 80-s.
Contemporary verifiers should do the same automatically.
- jasinjames 4y agoFascinating anecdote. Where can I read more about this?
- thesz 4y agoI don't know where you can read more. There are resources in Russian, but buran.ru is not quite functioning right now. I remember that story from the time when I worked with guys from Russian CQG team, who, in turn, worked in CQG with the member of the Buran's software engineering team. It was 15 years ago.
- xavxav 4y agoIndeed, Creusot itself is not formally verified, but we have verified the metatheory in our paper RustHornBelt: https://people.mpi-sws.org/~dreyer/papers/rusthornbelt/paper.pdf https://people.mpi-sws.org/~dreyer/papers/rusthornbelt/paper.... Actually verifying the translation that Creusot produces would definitely be interesting future work, but I'm not sure it's where the best 'bang for the buck' is found right now, though I try to ensure the underlying translation would remain simple to formalize.
- rowanG077 4y agoIs it guaranteed that Rust -> WhyML -> Rust Would ever yield a fixed point?
- thesz 4y agoIt is possible to produce a dump of Rust program AST into WhyML datatypes and/or functions and project and prove what can be proven. The structure of WhyML datatypes and functions can be parsed and transpiled back into Rust.
- Jweb_Guru 4y agoIn theory no. In practice probably (Rust compiles itself to a fixed point from older versions in around 3 iterations, IIRC).