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.
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).
First of all, welcome to my new blog. Being this my first post, I will present myself, give you some background on what I am doing and explain what are my intentions about this blog. My name is João Fernando Ferreira and I am a research student at the Foundations of Programming research group at the University of Nottingham (visit the About page to find out more).
My research is on algorithmic problem solving and its main goal is to develop calculational problem-solving techniques resulting in educational material supporting the use of a calculational approach to algorithmic problem solving. The focus of the project will be on the dynamics of problem solving – the processes of mathematical modelling and effective calculation in the formulation of concise and precise algorithmic methods.
As any other researcher, I spend most of my time reading and writing. That is one of the reasons I have created this blog: to organise my written notes. Using a blog system brings me some advantages like:
- I can tag my notes and use the system search capabilities to find them;
- I can access and change them from any place in the world, as long as I have Internet access;
- I can add new content from any place in the world, as well;
- I can share my notes and get feedback from my colleagues, supervisors, friends or anyone who is just interested in the same topics.
Other important reason to share my notes and thoughts is that I think they may be of interest for programmers. Since this is my first post, and (probably) most of you don’t really understand what I am doing, I will start by presenting some historical facts (mixed with personal opinions) and motivations. It is my hope that these facts will help you understand the relation and importance of mathematical methodology to programming. Please note that to read the entire post, you may need to click the “Read more” link.
In the 1960s, programmers started recognising that there were serious problems in the programming field and that it was necessary to prove the correctness of programs. At the time, software engineering was facing a software crisis and programming was not very well understood. Many software projects ran over budget and schedule and some of them even caused property damage and loss of life (see the RISKS-FORUM Digest for some examples).
To solve these problems, computer scientists focused on programming methodology and on ways to build programs in a systematic way. A common consensus was that programs should be proved correct, and in the late 1960s, some important articles had an important impact on the field. In 1968, Edsger W. Dijkstra published an article on the harmfulness of the Go To statement, where he claims that its use makes it impossible to determine the progress of a program. Also, one year later, Tony Hoare published a seminal article where he introduces the Hoare triples and an axiomatic approach to language definition.