We use the application domain of functional programming to explore the
first problem. We build a pattern-matching style recursive function
definition facility, based on mechanically proven wellfounded recursion
and induction theorems. Reasoning support is embodied by automatically
derived induction theorems, which are customised to the recursion
structure of definitions. This provides a powerful, guaranteed sound,
definition-and-reasoning facility for functions that strongly resemble
programs in languages such as ML or Haskell. We demonstrate this package
(called **TFL**) on several well-known challenge problems.

In spite of its power, the approach suffers from a low level of automation, because a termination relation must be supplied at function definition time. If humans are to be largely relieved of the task of proving termination, it must be possible for the act of defining a recursive function to be completely separate from the act of finding a termination relation for it and proving the ensuing termination conditions. We show how this separation can be achieved, while still preserving soundness. Building on this, we present a new way to define program schemes and prove high-level program transformations.

Since the second problem is largely social, we cannot solve it alone;
however, we do present an artifact that marks a path to a brighter
future. In particular, we show that the sophisticated algorithms
implemented in **TFL** can be parameterized by a higher
order logic proof system. The package has been instantiated to HOL and
Isabelle-HOL, two quite different mechanizations of higher order
logic. In this exercise, we found that the fully formal approach taken
to justifying definitions and deriving induction schemes was fundamental
in providing the required combination of portability and soundness.