What you're describing is more in the domain of program verification, there's already work like this, for instance dafny [1], where you can have functions like

What you're describing is more in the domain of program verification, there's already work like this, for instance dafny [1], where you can have functions like this: method Abs(x: int) returns (y: int) ensures 0 <= y { ... } or: method MultipleReturns(x: int, y: int) returns (more: int, less: int) requires 0 < y ensures less < x < more { more := x + y; less := x - y; } [1] https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ https://www.microsoft.com/en-us/research/project/dafny-a-lan...