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.
Although Hoare’s theory had a great impact, it was quite difficult to use it to prove existing programs correct, since one was forced to find an invariant for each loop. Programmers started studying alternatives, and the most plausible one was to develop the program together with its proof. Some years later, in 1975, Edsger W. Dijkstra published a paper where he introduced weakest preconditions. One year later he published the book “A Discipline of Programming” and showed how to use weakest preconditions as a “calculus for the derivation of programs”. Programmers were now able to build programs in a more reliable and systematic way, and the art of programming became more and more a discipline of programming.
From here, Dijkstra and others, dedicated themselves to the “mathematization” of programming and they learned to derive programs from their specifications: first simple ones, then more complicated programs. As the programs were becoming more and more complicated, the solutions were becoming less and less simple and beautiful. The reason was the “standard mathematical reasoning patterns” (see this note, page 9), which were not suitable for the task at hands. The conclusion was that computer scientists would have to learn how to construct proofs more effectively, in order to solve more ambitious problems. This was the beginning of a new period: computer scientists started to investigate ways of streamlining the mathematical argument. Mathematics and mathematicians were now faced with this new side of Computer Science.
During this new period, several problems were identified with traditional mathematics. One of the first problems was that mathematicians hardly manipulate their formulas: they interpret them; and one of the reasons is that the notation they use is not adequate for manipulation. This and other conclusions were also presented in the PhD thesis of Netty van Gasteren “On the shape of mathematical arguments“, where she presents a very interesting study about proofs (proofs of correctness of programs included).
My project is basically a continuation of Netty’s study, but while she did a breadth study, I am concerned specifically with algorithmic problems: construction of new algorithms and usage of algorithmic techniques to simplify mathematical invention.
Algorithms have been studied and developed since the beginning of civilisation, but, over the last decades, the unprecedented scale of programming problems and the consequent demands on precision and concision have made computer scientists hone their algorithmic problem-solving skills to a very fine degree.
Even so, and although much of mathematics is algorithmic in nature, the skills needed to formulate and solve algorithmic problems do not form an integral part of mathematics education; also, the teaching of computer-related topics at pre-university level focuses on enabling the student to be an effective user of information technology, rather than equip them with the skills to develop new applications or to solve new problems.
I believe that making clear the algorithmic nature of problems can help students understand what’s going on, and more importantly, they will be able to solve new problems more effectively. And since tomorrow’s programmers are today’s students, it is important that we learn how to streamline the mathematical argument, how to demystify the process of mathematical invention and how to turn the design of crisp arguments into a teachable discipline.
Thank you very much for reading my first post. It is already too long, so I will leave concrete examples and more detailed explanations — including derivation of programs from their specification — for later. I intend to write similar articles in the future, so if you like this one, consider subscribing this blog.