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
We’ll be tracking our progress on github and a site with more details on ongoing projects.
Join us on gitter or IRC (#wg-verification). We also have a mailing list.
The verification WG is mostly about how to verify software written in Rust, and concerned with things like tools that let you do that, and how the interaction between the developer, the compiler, and the tool should look like.
Eventually, the verification WG (and, in particular, the tool developers) will be a consumer of the memory model that the unsafe code guidelines team came up with.
I think the mailing list may be misconfigured. I wasn’t able to find it by searching the name (rust-verification) on Google Groups, and while manually entering the URL https://groups.google.com/forum/#!forum/rust-verification got me somewhere, the resulting page says “You must be a member of this group to view and participate in it.” (requiring manual approval even to view posts)
Is there any industry partners for this project yet? Something to use as a testbed/motivation for verification efforts? e.g. is there a component in firefox that’s particularly hungry for more robust verification?
Mostly I’ve been talking to Galois and some researchers over at ETH Zurich. These are two established tools that we can use to guide initial investigations. At various conferences/meetings, others have expressed interest.
Another inspiration for this WG is the excellent work that the NSS team has done with HACL*.
This should be viewed more as an investigatory/research-oriented WG with no immediate FF component target (in my opinion).
If you forgive some self-advertisement, I think that a participation of the Rust community to the ML and HOPE workshops at ICFP (see my previous announce thread on internals) could help further the goals of the Rust Verification WG.
To verify Rust programs, you need to have a semantics of everyday Rust code, while foundational verification efforts such as RustBelt naturally study a suitably aestheticized subset of the langague (sufficient to express everyday programs, but without syntactic sugar or features designed for convenience, such as lifetime inference or the pattern-matching ergonomics). In a community which decentralizes the surface language design through the RFC process and numerous working groups, the best way to ensure that clean, formalizable translations exist between the evolving surface language and those core/simplified languages is to (1) disseminate precise descriptions of ongoing/new language features and (2) teach the wider “internals” community to use and produce these precise descriptions.
Participating to academic workshops on language design is an engaging, low-cost way to get started on that front – and there are enough knowledgeable people in the Rust community to serve as mentors to produce nice submissions. Not everyone can build Iris, but anyone that has gone through the demanding process of language design by RFCs can submit and participate to ICFP-colocated workshops on language design. Consider submitting to the ML workshop! (And encouraging/helping your fellow rustaceans to do it.)
FYI, contrary to what Google says it is actually possible to join this group without getting a Google account. The usual way used to be to send an email to rust-verification+subscribe@googlegroups.com, but nowadays that just links you to Redirecting to Google Groups. That form, however, seems to have worked for me.
)