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-lan...