In the type-theoeretic world, you want to refer to "refinement types" [0]. Some interesting work that I have seen in this direction is Liquid Types [1][2]. Ther

In the type-theoeretic world, you want to refer to "refinement types" [0]. Some interesting work that I have seen in this direction is Liquid Types [1][2]. There is some work in Haskell[3], but it is surprisingly very useful in Rust as well. [0] https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type [1] https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/liquid-types/ https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/li... [2] https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf [3] https://ucsd-progsys.github.io/liquidhaskell/ https://ucsd-progsys.github.io/liquidhaskell/ [4] https://github.com/flux-rs/flux https://github.com/flux-rs/flux