Oleg Kiselyov, a prominent functional programming researcher, has advocated for using a language like Haskell or OCaml alongside or in place of equations where

Oleg Kiselyov, a prominent functional programming researcher, has advocated for using a language like Haskell or OCaml alongside or in place of equations where things like denotational semantics would usually be. I quote [0] Running [code] is a good thing because in Cartwright and Fellisen[1], [there is a] trivial typo (- instead of =). When you write things in TeX it's easy to make some mistakes, it's a good thing that it happens as a clear typo here but it could be a less clear typo and then it requires significant thinking [..] what was the correct thing. The advantage of using Haskell as a metalanguage is that if you replace = with - by mistake, almost certainly the compiler will not let you get away with this, you will catch it right away. Oleg does exactly this in [2]. If the sequent calculus-style rules put you off, there's an OCaml implementation! As an example I did this to the denotational semantics of R5RS Scheme, translating them to Haskell, the final result[3] is essentially a one-to-one mapping from the math to code. However there are some aspects of PL theory where you cannot write things as code directly (e.g. operational semantics, typing rules), and you have to resort to notation, but it's used pretty consistently. [0] https://youtu.be/GhERMBT7u4w?t=4395 https://youtu.be/GhERMBT7u4w?t=4395 [1] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.41.8026&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.41.... (typo fixed) [2] http://okmij.org/ftp/tagless-final/ski.pdf http://okmij.org/ftp/tagless-final/ski.pdf [3] https://github.com/siraben/r5rs-denot https://github.com/siraben/r5rs-denot