This is a nice post! Jeremy Siek wrote a similar post a few years ago:<p><a href="http://siek.blogspot.co.uk/2012/07/crash-course-on-notation-in-programming.html" rel="nofollow">http://siek.blogspot.co.uk/2012/07/crash-course-on-notation-...</a><p>If I could add one thing to these two posts, it would be to learn Prolog.<p>We write inference rules top-down ("from these premises, we draw this conclusion"), but we often read them bottom-up ("given this goal, what facts could have lead to it?").<p>This double-vision thing, where you simultaneously view a set of inference rules in both a deductive and goal-directed fashion, is IMO one of the main stumbling blocks for people new to type theory. Luckily[1], however, it's fundamentally the same intuition that Prolog programmers develop -- and learning new programming languages is usually easy for programmers.<p>[1] It's not really by luck, of course: Prolog is called a logic programming language for a reason...
This is great! I wish I had seen something like this years ago.<p>Related: "It's Time for a New Old Language" by Guy Steele.<p><a href="https://www.youtube.com/watch?v=7HKbjYqqPPQ" rel="nofollow">https://www.youtube.com/watch?v=7HKbjYqqPPQ</a><p>He gives a history of metalanguage notations (for both language semantics and syntax, including regexes and CFGs). And then he criticizes the inconsistency that has cropped up in these notations over the years.<p>The irony is that people who are formalizing precise semantics of programming languages do not agree on the syntax/semantics of the metalanguage.<p>I guess this is what you notice when you read hundreds of programming language papers, as I'm sure Guy Steele has.<p>-----<p>Also, does anyone know if what he refers to as "progress and preservation" are the same / related to "liveness and safety" in distributed algorithms? It sounds like the same kind of idea.