Towards a coding-like experience for mathematical proof writing

We introduce a new language for the purpose of writing formal mathematical proof. The design of the language borrows concepts and syntax from the Fitch notation, the C family of programming languages, and the Z formal specification notation. The intent is that the experience of writing a mathematical proof in the new language should feel like writing code in a modern, high-level programming language. In particular, the syntax should feel familiar to those with moderate exposure to programming languages in the C family, including, for example Java and C++. The language is text-based, meaning that the syntax prioritizes keywords over symbols and graphical devices, with the aim of making entry from a keyboard straightforward. Optionally, text-based proofs written in the language may be parsed and transformed to any presentation format, for instance LATEX, using tooling. We anticipate the language finding use cases in a variety of settings, including software-engineering, general engineering, data science, and education. Moreover, the simplicity of the language should present a gentle learning curve to the beginner or anyone who is curious about mathematical proof and wishes to learn the basics with a minimal investment of time and effort. With the ever increasing number of individuals working across a variety of technical disciplines, from engineering to data-science, who routinely write code occupationally, it would seem to be an ideal time to introduce a language that brings a coding-like experience to the process of writing mathematical proof.