= 27d567bc2d48d9f40e9ccc20ea370b15)
gjm comments on Second-Order Logic: The Controversy - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (188)
I don't know what you mean. Suppose you want a function A -> Int, where A is some type. \x:A. 6, the function which takes x (of type A) and outputs 6, seems to do fine. To put it in c-like form, int six(x) {return 6}.
If programs are proofs, then general programming languages correspond to trivialism.
Am I missing something?
The type on the right-hand side is usually something much more complicated and "creating an output of the desired type" is not trivial.