Re: Bridging the gap between application and proof

anakin_at_unitedsoftworks.com (Todd Bandrowsky) wrote in message news:<af3d9224.0306120715.600f95e2_at_posting.google.com>...
> The proof for pythagorean's theorem is of one square inside the other.
> You put one square inside the other, slightly tilted so that the
> subtraction of the areas leave four triangles. Basically you walk
> through the known areas of the two squares, given the lengths of their
> sides, and work it until you get pythagoreans theorem. A nifty web
> site that shows it is here:
>
> http://mathforum.org/isaac/problems/pythagthm.html
>
> There is of course a huge thread where I made the claim that a program
> could be a proof, and there are lot of people that vehemently disagree
> but without really saying why, except for the case of determinism.
> It bothers me that there is something magical about proofs such that
> they cannot be encoded.
>
> I were to write a program that says c^2 = a^2 + b^2, what could I do
> with just that?

Except you did not make the above assertion. Had you made the above assertion the response would have been "Well, duh!" Dijkstra et al have been saying the same thing for decades.

What you said was that full coverage test cases equate to proofs and that all programming languages are equivalent. Both of the assertions are absurd.

You argued against using mathematics, theory and proofs without even understanding that fact. You argued in favor of returning to the state of application specific databases we abandoned decades ago as ineffective and unworkable.

If you are going to make arguments in comp.databases.theory, I think the readers of the newsgroup would appreciate you first taking the time and effort to understand your own arguments! Received on Sat Jun 14 2003 - 05:04:43 CEST