Practical Idiomatic Considerations for Checkable Meta-Logic in Experimental Functional Programming

TL;DR

This paper introduces novel idioms in literate Haskell'98 to enhance the expressivity of checkable meta-logic, bridging simulation and formal specification for practical modeling and verification.

Contribution

It proposes new idioms like meta-language marking, nominal axiomatics, and constructive existentials to improve meta-logical annotations in functional programming.

Findings

Enhanced expressivity in checking frameworks

Application to realistic modeling problems

Practical idioms demonstrated in literate Haskell'98

Abstract

Implementing a complex concept as an executable model in a strongly typed, purely functional language hits a sweet spot between mere simulation and formal specification. For research and education it is often desirable to enrich the algorithmic code with meta-logical annotations, variously embodied as assertions, theorems or test cases. Checking frameworks use the inherent logical power of the functional paradigm to approximate theorem proving by heuristic testing. Here we propose several novel idioms to enhance the practical expressivity of checking, namely meta-language marking, nominal axiomatics, and constructive existentials. All of these are formulated in literate Haskell'98 with some common language extensions. Their use and impact are illustrated by application to a realistic modeling problem.