4 ms·
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 t
by username90 8y ago
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.
- sfvisser 8y agoBut 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.
- smadge 8y agoThat’s true but in most languages the things you prove are relatively obvious propositions like “(A and A)implies A.”
- MaxBarraclough 8y ago> 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?