r.g. recently I was working on a completely formalized proof (in the HOL4 theorem prover) of a routine to print out the value of an IEEE 754 floating point number.
So, OK, the program itself I can write in maybe 30 minutes. Difficulty: here we want a fully formalized proof of correctness in HOL4 (i.e. proof starts from logic and works its way up, a la Russell and Whitehead’s Principia Mathematica).
Let’s see: the definitions I’m going to need here are mostly obvious, in that they’re formalization of stuff that’s in the IEEE 754 standard: things like is_zero(), is_nan()...
Theorems are moderately obvious, in that what I want to say here is that the way you do it in the C runtime’s math.h works .. except, of course, we’re not doing this in C we’re doing it in ML, for provabilioty reasons.
On to the proofs. OMG, I need to prove some really stupid lemmas here; in that the lemma is Obviously True, but annoying to prove.
On to the proofs… well, I guess. case split on what type of floating point value we’re talking about (infinity? nan? zero? finite?), algebraically simplify...and we’re done.
At the other end of the formality scale … for one reason or another, I am looking at the Casimir Effect in quantum field theory. Gah, zeta summation. These guys are playing fast and loose here, mathematically. Like, no way in hell would I dare write down a formalization of what’s going here here.
r.g. recently I was working on a completely formalized proof (in the HOL4 theorem prover) of a routine to print out the value of an IEEE 754 floating point number.
So, OK, the program itself I can write in maybe 30 minutes. Difficulty: here we want a fully formalized proof of correctness in HOL4 (i.e. proof starts from logic and works its way up, a la Russell and Whitehead’s Principia Mathematica).
Let’s see: the definitions I’m going to need here are mostly obvious, in that they’re formalization of stuff that’s in the IEEE 754 standard: things like is_zero(), is_nan()...
Theorems are moderately obvious, in that what I want to say here is that the way you do it in the C runtime’s math.h works .. except, of course, we’re not doing this in C we’re doing it in ML, for provabilioty reasons.
On to the proofs. OMG, I need to prove some really stupid lemmas here; in that the lemma is Obviously True, but annoying to prove.
On to the proofs… well, I guess. case split on what type of floating point value we’re talking about (infinity? nan? zero? finite?), algebraically simplify...and we’re done.
At the other end of the formality scale … for one reason or another, I am looking at the Casimir Effect in quantum field theory. Gah, zeta summation. These guys are playing fast and loose here, mathematically. Like, no way in hell would I dare write down a formalization of what’s going here here.