Re: Bridging the gap between application and proof

Your posting sounds off-topic for comp.databases.theory, but might be more suited to comp.theory.

I'm, not an expert on this kind of stuff, but...

A while ago, I attended a talk where John Crossley pointed out that functional programs are basically proofs that are executed. His homepage is here - there are several papers that sound like they're about directly turning proofs into code;
http://www.csse.monash.edu.au/~jnc/

Also, you might be interested in;
http://www.research.avayalabs.com/user/wadler/papers/frege/frege.pdf (though, that document focusses primarily on types and not the code itself)

Whereas logic programming is basically automatic theorem proving.

-Benjamin Johnston

"Todd Bandrowsky" <anakin_at_unitedsoftworks.com> 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?
Received on Sat Jun 14 2003 - 04:37:27 CEST