NummSquared: a New Foundation for Formal Methods

To spread the use of formal methods, a language must appeal to programmers, mathematicians and logicians. Set theory is the standard mathematical foundation, but often ignores computational aspects. Type theory has good support for mixing specification and implementation, but often imposes type constraints in excess of those found in typical programming languages. Furthermore, standard mathematics is untyped. Languages based on the untyped lambda calculus often permit non-terminating programs and require reasoning in non-classical logics. Languages without higher order functions often lack polymorphism. There is a wide gap between con-ventional programming languages and logic. This paper proposes NummSquared, a new formal language based only on untyped higher order functions, which allows only terminating programs, has a classical logic, is related to well-founded set theory, and supports reflection. NummSquared supports rapid prototyping without proofs to reduce cost, and supports adding proofs later. 1 Overview and comparison A feature that is elegant in a programming language may be inappropriate for formal methods, particularly when the programming language must also serve as a logic. The untyped lambda calculus, a useful model for many program-ming languages, is elegant because it is based only on untyped functions, and any function may be passed as an ar