Modulbeschreibung

Although widespread, the currently mainstream imperative, object-oriented programming paradigm, with testing as its main method of quality assurance, has its limitations. Even though it allows novices to write programs relatively quickly and without much formal training, such programs tend to become complicated as soon as they need to do something non-trivial. This makes them increasingly hard to write and reason about, making assurance methods that give better guarantees than software testing intractable. Similarly, even though it is possible to write software tests relatively quickly and without much formal training, such tests are only able to show the presence of faults, but never their absence.

Few are aware that there exist a number of alternatives to imperative, object-oriented programming and testing. This course will focus on one of them, functional programming, and the use of formal methods to specify and prove the correctness of functional programs. 

Functional programming is an approach to programming where simplicity, clarity, and elegance are the key goals. It is the application of formal mathematical and programming-language-based techniques for the construction and verification of computer programs. Although it has a long history, it has recently received attention due to its potential for writing elegant, correct and efficient programs that are easier to write, compose, and maintain, once one is familiar with its underlying concepts. Its simplicity also allows reasoning about the correctness of functional programs using techniques taught in high-school mathematics. These techniques can not only be used to state and prove functional correctness of smaller programs on paper, but also large systems using automated proof assistants. Such automated proof assistants (e.g. Agda, Isabelle/HOL, Idris, Lean and Coq) are themselves applications and further developments of functional programming.

Main Aim: All participants are able to explain and apply formal programming-language-based techniques for the construction and verification of computer programs. Special emphasis will be made on techniques that surpass some of the limitations of mainstream programming in the imperative object oriented programming style, and on alternatives to mainstream quality assurance using unit testing.

In particular, all participants should be able to:

• construct programs in the functional style.
• verify the correctness of programs using property-based testing and proof.
• explain the formal foundations of the techniques covered.

The functional programming language Haskell will be used as a basis whenever appropriate.