What would it take to add refinement types to Rust?

Y	Hacker News new \| ask \| show \| jobs

	What would it take to add refinement types to Rust? (yoric.github.io)
	26 points by leosarev 541 days ago

3 comments

conradludgate 540 days ago

For what it's worth, with the uom[0] crate you can represent that type equality. It represents units as powers of SI units, so m^1s^-2. It does not have the nice error messages though

[0] https://docs.rs/uom/latest/uom/

link

deterministic 538 days ago

Having refinement types in Rust would be a massive game changer. It would make it possible to write proven correct software directly in Rust. Hey even I would switch from C++ to Rust :)

link

fn-mote 540 days ago

Author has made significant contributions to Rust. This is a very serious article.

link