So the question is: Can we carry out formal reasoning on programs? The answer is in this slide: formal reasoning indeed is viable. And how is it viable? Typed functional programming does offer some answers and some help. Why is this the case? Typed functional programming first of all enforces a declarative paradigm on the user and thus it allows the user to express computations and programs directly in mathematics. Moreover, by means of expressive type disciplines, remember we are not talking just of functional programming but of typed-functional programming, by means of expressive type disciplines and module systems users can treat systems and program components as mathematical objects themselves. And so natural formal methods arise in this context.
In particular there are two areas where formal methods are very successful. One of them is program development, especially through the technique of so-called data refinement and program transformation. And the other is program verification. Here I have listed some of the major applications. In program transformation calculi are particularly useful to overcome efficiency issues. You know functional programming has often been challenged not to be sufficiently efficient. These are tools which allow to improve that. And here is a list of logical principles, which naturally arise in connection with functional programs.
