There's also Idris, which I haven't really used, but from what I understand, it's sort of like Haskell with dependent types.
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
{
...
} method MultipleReturns(x: int, y: int) returns (more: int, less: int)
requires 0 < y
ensures less < x < more
{
more := x + y;
less := x - y;
}
LiquidHaskell is nice because it's all written in comments next to or in a separate file from your Haskell code. This means the Haskell compiler doesn't even have to know about it. On the other hand, when you're using something like Idris for formal programming, you often find your program full of proof witnesses that you aren't actually using for your real code you want to write. You can prove all sorts of things, like that a function only returns negative multiples of 3, or only returns vectors of length 5n+1.
The latest proposal is P0380, "A Contract Design": https://wg21.link/P0380.
An earlier work, "Simple Contracts for C++" (https://wg21.link/P0287), gives some further background and motivation.
Notably, contracts are currently solely in the proposal stage (and not in the upcoming standard).
The current concept proposal is significantly reduced in scope and doesn't include anything like axioms.
It isn't as clean, but it does the job.
For example you could have a PositiveNumber class, with the mathematical operators overloaded that always validated the invariant of the number being positive.
For example in the Number concept, can you have a PositiveNumber concept (e.g., require Number > 0)? Or given some container, that it is sorted? Or if you have a binary operator, that it is associative?
Maybe with some magical compiler that can tell you that after calling abs() or exp() the "double" type becomes a positive number concept, or that after calling sort on a vector and only doing binary inserts that the vector is still sorted.
Basically a lot of contracts on how to use a function correctly is not captured by just type system or whether you can call certain functions on a type. Is there an easy way to attach a "concept" to an output in an ad hoc way?