A program proves nothing at all so I am not sure what you can understand from it? Typically in programming you are presented with a piece of code, a statement that this piece of code solves a specific problem and then a proof of that it actually works. Those proofs are typically far from understandable or rigorous.
> Typically in programming you are presented with a piece of code, a statement that this piece of code solves a specific problem and then a proof of that it actually works.
Not really. It's quite unusual to see a serious formal approach.
I'm working through a book that uses C++. Every few pages I find undefined behaviour (struct punning, illegal use of memset to zero-out objects, etc) and needless usage of non-standard compiler-specific language features.
This is the well it works on my machine mindset used widely in programming, even in books written by highly qualified people.
> Those proofs are typically far from understandable or rigorous.
I'm not sure what kind of thing you're thinking of here. Can you give an example?
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.
