Formal Methods within a Totally Functional Approach to Programming, in B.K. Aichernig and T. Maibaum Eds., Formal Methods at the Crossroads: from Panacea to Foundational Support

Abstract. Taking functional programming to its extremities in search of sim-plicity still requires integration with other development (e.g. formal) methods. Induction is the key to deriving and verifying functional programs, but can be simplified through packaging proofs with functions, particularly “folds”, on data (structures). “Totally Functional Programming ” avoids the complexities of interpretation by directly representing data (structures) as “platonic combina-tors ”- the functions characteristic to the data. The link between the two simpli-fications is that platonic combinators are a kind of partially-applied fold, which means that platonic combinators inherit fold-theoretic properties, but with some apparent simplifications due to the platonic combinator representation. How-ever, despite observable behaviour within functional programming that suggests that TFP is widely-applicable, significant work remains before TFP as such could be widely adopted. 1 Programming Is Too Hard There can be little doubt that “programming ” (both as metaphor for and essence of th