sure: Refinement Types in (unstable) Rust

178 points Lasuman 20 comments

I've been working on this for the past few weeks, and just did the first very early release on crates.io! (Docs aren't able to build because next solver isn't supported on docs.rs)

This crate leverages const-generics to encode the possible values of a type and is able to track and update these possible values through operations.

Right now the primary focus is on the std integer types, but this same concept is applicable to many other types as well.

The vast majority of integer ops and methods are already supported.

Why would anyone want this? :

Apart from just putting as much information as possible into my types being just fun on its own, your program compiling proves that you will never have overflows at runtime (or rather, no "erroneous" overflows, the `wrapping_*` methods exist after all).

Additionally this is a 0-cost abstraction on top of plain integer maths, the only cost you pay is at compile time (which can take an arbitrarily long time :] ).

I would appreciate any and all feedback, ideas for additions like methods, helper macros etc, or what you think I could improve in general ^^

(I am the sole contributor to this project, this repo is free from LLM-generated code.)