Re: How does Curry/Howard formalize PROGRAM calculates FUNCTION (W&S?)


george wrote:
Charlie-Boo wrote:
george wrote:

The issue IS NOT whether the program satisfies ME!
The issue IS whether the program satisfies THE SPECIFICATION!
Since in this case, the program IS the specification,

That's not a specification for a program.

It IS SO TOO, dumbass.

It's a program being
compiled/translated.

It's THE SAME THING, dumbass.
What you, in your utter stupidity, CALL program
synthesis, is just compilation. Compilers have source
code as input and object code as output.
They translate one into the other.

Are you aware of the difference between expressing a relation and
representing it?

C-B

What you call "program synthesis" is doing the
exact same thing, just with a 3rd-generation language
as the object code and some as-yet-un-understood-by-
you higher-level "specification language" as the source
"code". I put "code" in quotes because anything that
actually counts as a specification language is TOO INformal
TO BE code. If it were formal enough to be code, then,
precisely as I said, what YOU are CALLING a "program
synthesizer" from that language WOULD JUST BE a COMPILER for it.

.

Quantcast