Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

But programs are proofs!

At least in the light of the Curry–Howard correspondence. :)

Anyways, I do agree that in programming it’s easier to see what are introductions, assumptions, definitions, functions, values etc. You can’t just invent a notation and go with it. Everything needs to be defined from the ground up. It’s constructive and I like that, probably because I’m a programmer.



That’s true but in most languages the things you prove are relatively obvious propositions like “(A and A)implies A.”




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: