[zasdffaa]

I've had a quick look over your posts, and I will look over the more carefully as a refresher on these kinds of things (I have looked at Hoare logic which this resembles, and a couple of other related things). The problem is to me, the formal semantics aren't actually very different from what you would write in English, and the real problem, and this is never addressed, how do I use this (which includes: how do I manipulate these things symbolically to some useful end)? The reason I don't get more deeply stuck into these formal semantics is because they seem to have no way for me to actually do anything useful with them. This lack of a 'bridge' is a huge problem to me because I can't justify learning that which appears of no use.

Any comments appreciated, and don't be put off by the negative tone of this, it's just frustration.

[azdavis]

The biggest reason why you'd want a formal semantics for your PL, as opposed to just a "human" language specification, is so that you can do proofs about the formal semantics. You can prove your PL, as defined, satisfies certain "safety" properties. And the point of doing these proofs is is to check that the definition of the PL "makes sense".

PLs that don't have a formal semantics (aka, most mainstream PLs) are more likely to be in situations where implementors realize, after the standard has been written, that e.g. some of the PL's features interact in a way that doesn't make sense, such as this example with C++ coroutines and lambdas: https://news.ycombinator.com/item?id=33084431

Two of the most common safety properties of interest are progress and preservation. (I touched on this in the last above linked post near the bottom.) At a high level:

1. Progress states that if you have a program that type-checks, then either that program is "done" or it can continue evaluating.

2. Preservation states that if you have a program that type-checks and that can continue evaluating, then as it continues to evaluate, it continues to type-check.

Note that the conclusion of preservation "feeds back" into progress: the program type-checks. And vice versa: progress may state as its conclusion that the program can continue evaluating, which then lets you apply preservation. This means you can keep applying the progress and preservation theorems in a "loop" until the program is done evaluating.

For each of the 4 posts in my series about formal semantics, I duly translated the rules presented in the blog post into Lean code, and then proved that the rules do satisfy the safety properties. For example, for the first post linked above:

- The syntax of the language: https://github.com/azdavis/hatsugen/blob/part-01/src/syntax....

- The static semantics (the "typechecker"): https://github.com/azdavis/hatsugen/blob/part-01/src/statics...

- The dynamic semantics (the "runtime"): https://github.com/azdavis/hatsugen/blob/part-01/src/dynamic...

- The proofs of safety: https://github.com/azdavis/hatsugen/blob/part-01/src/safety....

[zasdffaa]

I have a background in formal methods and PLs, and never used it. I understand the supposed benefits but IME they never got used.

Clearly you have used it, so I'll take time looking over your stuff (though I don't know lean).

I appreciate you taking the time to write a comprehensive answer, as I said, I'll try to do it justice!