At the recent Rust work week in Berlin, we formed a working group to investigate formal methods in Rust. The scope of this working group ranges from projects like RustBelt that are intended to develop a formal foundation for the language to projects that will directly analyze Rust programs.
Our goals are to provide a central location where we can gather and share information on ongoing efforts. As we make progress, we’d like to look at integration with testing frameworks to provide “testing on steroids.” Our first priorities are currently:
- extracting required information from the compiler (e.g. trait impls, types)
- writing example specifications to help design a common, extensible way to write annotations on Rust programs
Welcome to Rust’s first formal working group ( )