Extraction of Rust code from the Why3 verification platform

Sammanfattning: It is hard to ensure correctness as software grows more complex. There are many ways to tackle this problem. Improved documentation can prevent misunderstandings what an interface does. Well built abstractions can prevent some kinds of misuse. Tests can find errors, but unless they are exhaustive, they can never guarantee the absence of errors. The use of formal methods can improve the reliability of software. This work uses the Why3 program verification platform to produce Rust code. Possible semantic-preserving mappings from WhyML to Rust are evaluated, and a subset of the mappings are automated using Why3's extraction framework.