Functional programming systems provide a number of features which facilitate program verification. Such verification may be observed to rest directly upon the theoretical foundations of computing and simultaneously to exhibit a close relation to the programs being verified.

In order to demonstrate these aspects of functional systems, two functions, MIN and SORT, are defined on a parameterized type consisting of sequences to elements from some ordered type. Theorems showing that MIN and SORT terminate and return the correct values are stated and proved. Similar results are derived for a function to perform a binary search on an ordered sequence.

Finally, conditions similar to Dijkstra’s weakest preconditions are given which allow the simultaneous synthesis and verification of certain programs from program specifications. A function to find the greatest common division of two integers is derived and verified.