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


Jan Burse wrote:
george wrote:
syntactically correct program gives SOME function. The only
way to allege that some other function should've been given
instead is to use some OTHER HIGHER-level language to specify
the function; the question then becomes whether we have correctly
translated the function out of that natural language into this formal

I cannot share this view of what a program
is and what in relation to a program a
specification might be.

Oh, shut up. The truth is the precise opposite;
you cannot NOT share it. This is just the way it is,
and you do in fact agree with it despite your knee-jerk
tendentiousness, which is psychology getting in the way
of epistemology.


One can use the same an only formal language
for specifications and programms.

Only if one is either a) stupid, or b) completely
ignorant of the PURPOSE of a *specification*.
If the program and the specification can be written
in the same language, and are, then guess what:
the specification IS the program, so, having written
the specification, YOU JUST COMPILE IT AND RUN IT,
and voila.

.

Relevant Pages