BLEG: Curry-Howard equates (proposition, proof) to (type, function). What equates it to computation (state, trace)? Russell-Whitehead?
Russell-Whitehead correspondance: propositions as states of your formal system, proofs as transition traces from one proposition to another.
-
-
A proposition is a type; it can describe the shape of your state, but how would it describe the state itself?
-
In Russell-Whitehead, a proposition is a state of the machine itself: a sequence of symbols denoting what has been deduced so far.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
Read my blog!