azdavis

Hope it’s helpful!

The main motivator for why I did this is because we use SML as a teaching language at my university and students always seem to struggle with the error messages and tooling from the compiler.

- https://matklad.github.io/2023/08/01/on-modularity-of-lexica...

- https://azdavis.net/posts/pl-idea-tooling/

I think pure functions, sum/product types, and pattern matching are generally accepted as an excellent way to model and manipulate pure data. I wonder what the team’s thoughts are about handling less pure things like asynchrony and I/O, as well as more interesting control flow like exceptions/panicking, coroutines, generators, iterators, etc.

There’s also https://smlhelp.github.io/book/ which is mostly put together by current/past CMU students.

Note: I made Millet.

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....

There was some past discussion about it on HN: https://news.ycombinator.com/item?id=32512715

For my part, I think it’s unfortunate that virtually no mainstream language has a formal semantics in the style of SML’s Definition. I wrote a bit about formal programming language semantics in a series of posts: https://azdavis.net/posts/define-pl-01/