[quotemstr]

All I want for Christmas is a programming language that uses dependant typing to make floating point precision part of the type system. Catastrophic cancellation should be a compiler error if you assign the output to a float with better ulps than you get with worst case operands.

[thesuperbigfrog]

Ada might have what you want:

https://www.jviotti.com/2017/12/05/an-introduction-to-adas-s...

http://www.ada-auth.org/standards/22rm/html/RM-3-5-7.html

http://www.ada-auth.org/standards/22rm/html/RM-A-5-3.html

Ada also has fixed point types:

http://www.ada-auth.org/standards/22rm/html/RM-3-5-9.html