I wonder how pragmatic those can become. Usually I don't really care about "exact" exactness, a common theme in haskell. A sort of "under common assumptions" (no underflow/overflow/OOM etc.) proof of laws and properties. This eliminates a whole class of bugs and strengthens your ability to reason, but doesn't make everything super, super complicated by thinking about all those edge cases.

One usually doesn't program airplane control software. Some bugs are okay and speed of development and correctness is a trade-off.