3 ms·

> Imagine mathematicians or computer scientists re-proving real analysis theorems using floating point arithmetic... Mathematicians and computer scientists do

> Imagine mathematicians or computer scientists re-proving real analysis theorems using floating point arithmetic... Mathematicians and computer scientists do prove theorems about floating point arithmetic! For example, the most widely-cited floating point reference contains no fewer than fifteen theorems about floating point: http://docs.oracle.com/cd/E19957-01/806-3568/ncg_goldberg.html http://docs.oracle.com/cd/E19957-01/806-3568/ncg_goldberg.ht... Or here's a presentation about representing functions with their Taylor expansions using floating point arithmetic, providing strong error bounds on the result of adding or multiplying two functions represented in this way: http://perso.ens-lyon.fr/nathalie.revol/talks/ICIAM07.pdf http://perso.ens-lyon.fr/nathalie.revol/talks/ICIAM07.pdf I agree that many proofs in computer science are harder than proofs in mathematics, because you can't deal with idealizations - you always have to think about the machine. But unlike empirical sciences, we have access to the design of the machine. We know what many of the axioms are. Formal reasoning is valid for a far larger part of computer science than for the natural sciences. I'm not going to argue that proofs are a panacea for every situation. But I also don't categorically reject them in the domains where they can be usefully applied.

stiff 13y ago
I know there are theorems about floating point, that's missing the point, what I am saying is that the theories most useful for doing reasoning are often nearly impossible to formulate if you would like to include in them a lot of messy details of something like floating point, just as one example. What happens instead, we reason using nice idealized theories, and then we experiment to asses the gap between theory and reality. I am completely a fan of theory and proofs, but the point of the quoted comment is that there is an empirical component to software development too, and your original comment seemed to question it.
astrodust 13y ago
A theory, no matter how well defined, will never, ever, precisely match reality. Testing is not optional. Why are you implying you can proof your way around this? A "proof" is useful for some problems, but I'll take very rigorous real-world tests over a proof any day.

stiff 13y ago

I know there are theorems about floating point, that's missing the point, what I am saying is that the theories most useful for doing reasoning are often nearly impossible to formulate if you would like to include in them a lot of messy details of something like floating point, just as one example. What happens instead, we reason using nice idealized theories, and then we experiment to asses the gap between theory and reality. I am completely a fan of theory and proofs, but the point of the quoted comment is that there is an empirical component to software development too, and your original comment seemed to question it.

astrodust 13y ago

A theory, no matter how well defined, will never, ever, precisely match reality. Testing is not optional. Why are you implying you can proof your way around this? A "proof" is useful for some problems, but I'll take very rigorous real-world tests over a proof any day.