How are computer programs constructed? The usual way is that programmers get a (usually too vague) description of what is wanted, and then just start programming. Everybody will agree that this is not the right method: too often it goes wrong, and the production of software is too expensive. But then, what is the good way?
In algorithmics, also known as the mathematics of program construction, one looks at formal methods to construct programs. The most important question is not so much how a program can be derived from a specification, but rather how that can be done effectively and efficiently (and elegantly).
Looking at international research on this subject, there appears to be much attention for the method of program transformation: derive a program in a step-by-step way through a series of "transformations" that preserve the meaning and hence the correctness. A significant practical problem is that very many steps seem needed: the individual steps are too small. In algorithmics a solution to this problem is searched for: formalisms and theories are developed with which a whole series of little steps can be combined into one single step at a higher level. Compare this with the development of higher programming languages: these make it possible to express compactly what needs many instructions in an assembler language. It also resembles the way mathematics is built up with concepts, notations, and theorems that are used in later proofs.
An important source of inspiration for the research are concrete algorithms, or rather classes of algorithms. For instance, what is the essence of parsing methods, or of shortest path methods? How can we express the derivation of these algorithms in a clear and succinct way? What systematic theory can be set up? In this research quite fundamental questions pop up, that can be well studied with tools like category theory and type theory. And besides theory formation, there is also an important more practical aspect: the development of tools that support this formal method of program construction, like ``incremental proof editors''.