Today’s programming languages are often characterised as either being:
- good for writing efficient code,
- good for verification, or
- easy to write and learn.
It is rare to find a programming language that is good for two of the above, let alone all of them. Research into Programming Language Design and Verification aims to achieve such an ideal programming language. In addition, we want a language that is:
- helpful when writing code collaboratively
- easy to read and understand
Programming languages are a fundamental tool for helping humans communicate with computers. Traditionally, programming languages are used with a compiler or interpreter (in the case of Java: both) for conveniently giving tasks to the computer. Meanwhile, program verification is used to ensure that the program given for interpretation or compilation indeed describes the tasks that were intended. This means that programming has become a form of two-way communication. Indeed, even a primitive form of program verification: static type checking, is considered a useful form of feedback for many programmers. While the Curry-Howard correspondence teaches us that program verification does not need anything but a sufficiently powerful type system, seeing program verification as a form of communication between a human and a computer shows that a lot can be improved.
Recognising that different domains require different solutions, it is possible that an ideal programming language may not exist. When focusing on finding new languages suitable for verification, there are several directions in which we hope to find solutions. One option is to create a meta-programming language with which many different DSL’s can be created, for which verification and efficient programming go hand in hand. Another option is to create an extensible language flexible enough to tailor for different needs, providing a basis in generating efficient code for different platforms while focussing on verification. Finally, we may be able to fundamentally change the way we think about programming. All of these are options I aim to try and play with through the development of the Amperspiegel tool.