Dec 222024
 

A few years ago, on a whim, I wrote YAIOUOM. YAOIOUM was a static analyzer for Rust that checked that the code
was using units of measures correctly, e.g. a distance in meters is not a distance in centimeters, dividing meters
by seconds gave you a value in m / s (aka m * s^-1).
YAIOUOM was an example of a refinement type system, i.e. a type system that does its work after another type
system has already done its work. It was purely static, users could add new units in about
one line of code, and it was actually surprisingly easy to write. It also couldn’t be written within the Rust
type system, in part because I wanted legible error messages,…

External feed Read More at the Source: https://yoric.github.io/post/rust-refinement-types/

 2024-12-22  No Responses »