Engineering the Prover Interface

Practical prover interfaces are sizeable pieces of software, whose construction and maintenance requires an extensive amount of effort and resources. This paper addresses the engineering aspects of such developments. Using non-functional properties as quality attributes for software, we discuss which properties are particularly relevant to prover interfaces and demonstrate, by the example of the I3P interface for Isabelle, how judicious architectural and design decisions lead to an interface software possessing these properties. By a comparison with other proposed interfaces, we argue that our considerations can be applied beyond the example project.