In the last post I have presented some historical context about programming and mathematical methodology. If you read it, then you should have an idea when and why programmers started to investigate on mathematical methodology. However, I haven’t mentioned any aspects of mathematical methodology that can help us to improve our programming or mathematical skills.
In this post, I’ll talk about mathematical proofs. And what’s the relevance of this topic to programmers? Well, computer programs are mathematical formulae, with a precise formal meaning and embodying constructive theorems about the systems they implement (as well-written in “Mathematics and Programming – A Revolution in the Art of Effective Reasoning”, by Roland Backhouse). The difference between theorems embodied by computer programs and the ones usually studied in mathematics is that they are applied by an unforgiving machine, with the effect that the smallest error can cause a huge damage. This means that computer programmers must create trustworth designs, i.e., the constructive theorems embodied by their programs must be programmed correctly.
Mathematical Proofs
Mathematicians job is to do mathematics, i.e., to design and present theorems, arguments, algorithms and in some cases whole theories. However, the traditional mathematical curriculum is more concerned with teaching mathematical facts — existing theories and concepts — than with the doing of mathematics. And even when design and presentation get some attention, they are treated separately: design of solutions is viewed as a psychological issue, while presentation is viewed as a matter of personal style (words from this Dijkstra’s note on Mathematical Methodology).
Continue reading