[billfruit]

But at least all imperative procedural steps are clearly understandable from source code given in many programming books. Where as maths books routinely leave out many steps in proofs and calculations, on top of many ambiguously used notations and terminology that can leave a self-student confused.

[username90]

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.

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

[sfvisser]

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.

[smadge]

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