Rust: Beyond the Typechecker

The specificity of Rust’s type system is that it is capable of guaranteeing that your program is memory safe and data-race free, two properties associated to categories of bugs both dreaded and notoriously hard to debug in C or C++. In each case, I identified a piece of code that could benefit from some verification; then I manually translated the Rust code into functionally equivalent pure F* code and proved some properties on the F* code that increase our confidence on the Rust code. Rather, the focus of my PhD will be to go beyond the typechecker and enable gradual verification of higher-level properties about Rust code, some examples of which can be seen in the case studies.

Source: blog.merigoux.ovh