> 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?
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?