What is missing to let users develop refinement type systems?

(apologies if this should be on users.rust-lang.org)

The Rust type system is powerful, but, by design, not all-powerful. There are properties that the Rust type system cannot encode (or at least cannot encode well) and quite possibly never will.

There is value in writing refinement type systems or other static analysis tools that take as input a well-typed Rust AST annotated with full type and span information, in order to perform further static analysis from said AST.

Example: A few years ago, I wrote a refinement type system for Rust, implementing Andrew Kennedy's-style units of measure. This was fun, it worked nicely, but it could only work with nightly and, as expected, it broke very quickly with updates to the compiler.

How far are we from having a stable API that could be used for this purpose? Or, if providing a stable API is too much of a burden, a sufficiently-stable export format?

You might be interested in Welcome - Rust Formal Methods Interest Group

2 Likes

Would stable mir be too low level? rust/compiler/stable_mir/README.md at master · rust-lang/rust · GitHub

I think that it would work for my use case. If I understand correctly, this hasn't reached 0.1.0, though, right?

Yeah, very WIP from what I can tell. So far the best option has been the internal crates though, so you're not worse off..

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.