How to make your papers run: Executable formal semantics for your language - Tweag
This post will show a simple example of how to use Makam, a very powerful, not yet widely-known, programming language to specify executable semantics of a simply typed lambda calculus with recursion and numbers (PCF).
I’m using Makam during my internship at Tweag to specify and experiment with the design of a new configuration language. Makam allows me to try new ideas quickly, without worrying about low-level details. In the long run, it’ll also work as documentation for the language.
A woman is relaxing on a chair on the beach, clearly on vacation, drinking an ice-cold drink. Her phone beeps. The text message asks ‘Can you come back to the office? We upgraded the compiler and the program you wrote last week stopped working’.
Ok, I might have exaggerated a bit, but every programmer has likely found themself, at least once, trying to understand why a program that was working with compiler A, suddenly stopped working when switching to compiler B. Or even worse, maybe it was working with compiler A, version 4.5.64, and it stopped after an update to version 4.6.23.
Ideally, programming language designers and implementors would like to keep this kind of situation to a minimum. And, when it does happen, they’d like to have a definitive answer as to how the compiler should behave. A specification. A ground truth.
