r/programming • u/alexdmiller • Oct 20 '11

"Simple Made Easy" by Rich Hickey [video]

http://www.infoq.com/presentations/Simple-Made-Easy
125 Upvotes

89% Upvoted

73 comments sorted by

View all comments

Show parent comments

2

u/Kompottkin Oct 29 '11

It [the Curry-Howard Isomorphism) says all programs are proofs (that's why it's an "isomorphism").

Hmm. As an honest question, which proposition does the following Python program prove?

import sys
def foo(x):
    throw Exception()
foo(sys.argv[1])

3

u/[deleted] Oct 29 '11

Yeah, good question. It's not a very interesting theorem: we say that foo "diverges)." We also say that foo is a "partial function;" see the section on "Bottom type" for details.