> In fact, 0.1+0.2 is likely != 0.3 for most software. This seems like a rather silly example: you're presumably talking about floating point numbers, but we h

> In fact, 0.1+0.2 is likely != 0.3 for most software. This seems like a rather silly example: you're presumably talking about floating point numbers, but we have a spec for floating point, it's IEEE 754. This spec has been formalised in many proof systems, e.g. (top Google hits for various systems I know): https://github.com/coq-contribs/ieee754 https://agda.readthedocs.io/en/v2.5.4/language/built-ins.html#floats https://www.isa-afp.org/entries/IEEE_Floating_Point.html I'm tempted to say that using integers/rationals/reals in a proof, when the software uses 64bit words and floats, is a rookie mistake; yet I've never even seen rookies make that mistake. Maybe that's a problem for approaches which keep programs and proofs separate, but in systems based on type-checking (e.g. Agda and Coq) it wouldn't even be possible to make such a mistake (there's no way to use different types in the program and the proof, since the program is the proof). > You can prove you have integer types or fractional types or whatever, then a hardware bug comes along and your proof doesn't relate to the real world anyway. I'd be very happy if hardware bugs were the main cause of my software's problems ;) More seriously, this seems like moving the goalposts from "is it useful?" to "is it perfect?".