[MaxBarraclough]

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