CTP-based programming languages? Considerations about an experimental design

This paper discusses plans for joint work in order to gain early feedback from the community. Three lines of work pursued independently so far shall be joined: (1) narrowing the gap between declarative program spec-ification and program generation already working in Isabelle, (2) reusing work, which embedded an input-response-loop re-sembling Computer Algebra Systems (CAS) into HOL Light, and (3) reconstructing an experimental language for applied mathe-matics by exploiting established as well as emerging features of Isabelle/Isar. These plans have to be seen as part of a variety of highly ac-tive research areas — on “integration of the deduction and the computational power ” of Computer Theorem Proving (CTP) and CAS respectively (Calculemus), on “innovative theoretical and technological solutions for content-based systems ” (MKM), on “Programming Languages for Mechanized Mathematics Systems” (PLMMS), just to cite from some related interest groups. Facing the abundant variety of approaches, of intermediate re-sults and of ongoing developments, and taking under considera-tion the many difficulties in integrating such approaches, we pursue pragmatic goals: Design a component indispensable for working engineers, a programming language for engineering applications. Use Isabelle for an experimental embedding of the language, which is useful at least in engineering education as soon as possible