Meeting proposal: State of formal methods tools in Rust

[xldenis]

Meeting proposal info

• Title: The state of formal methods tools in Rust
• Type: technical

Summary

There is a nascent community of formal methods tool developers for Rust, who make atypical but heavy usage of the compiler apis and infrastructure. In this meeting I hope to share how FM tool developers use rustc, their needs, the difficulties they encounter and potential solutions and enhancements. I hope that by bringing these issues to the attention of t-compiler, we can help to make Rust the language with the best formal verification infrastructure and tooling!

Note: I am currently writing a long document to provide context to be provided before any actual meeting.

About this issue

This issue corresponds to a meeting proposal for the compiler team steering meeting. It corresponds to a possible topic of discussion. You can read more about the steering meeting procedure here.

Comment policy

These issues are meant to be used as an "announcements channel" regarding the proposal, and not as a place to discuss the technical details. Feel free to subscribe to updates. We'll post comments when reviewing the proposal in meetings or making a scheduling decision. In the meantime, if you have questions or ideas, ping the proposers on Zulip (or elsewhere).

[xldenis]

I've written a document here: https://hackmd.io/CuEgMe-oSau4oj2UwNSx4g .

[bjorn3]

Left a couple of inline comments.

[pnkfelix]

We met on 2022-03-25

We discussed this doc: https://hackmd.io/qLk-wnwtStOhCOBeF5YuOw?view

The public zulip archive will serve as the meeting record: https://rust-lang.zulipchat.com/#narrow/stream/238009-t-compiler.2Fmeetings/topic/.5Bsteering.20meeting.5D.202022-03-25.20compiler-team.23488.2C.20.23498/near/276622720