azdavis

Nice post, I like the benchmarking and property testing. I had a somewhat similar post: https://azdavis.net/posts/unrecur/

Thanks! But I don’t think it quite worked?

I wrote a small post on that: https://azdavis.net/posts/lambda-cube/

Hope it’s helpful!

This is likely in response to https://news.ycombinator.com/item?id=43863937

I didn’t realize that “docs like code” was a noun phrase and was trying to figure out how docs can be liking code that is in basic terms.

Might this help? I wrote it: https://azdavis.net/posts/define-pl-01/

SML pops up now and again on HN, which is always nice to see. I wrote a language server for SML in an attempt to improve the tooling situation around the language: https://azdavis.net/posts/millet/

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.

I made a language server for SML with a focus on attempting to provide good error messages: https://azdavis.net/posts/millet/

Glad to see new languages designed around having good support for IDEs. matklad (rust analyzer) and I wrote a bit about this:

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

For the IDE use case, I made a language server for SML: https://azdavis.net/posts/millet/

For editor support for Standard ML you can try Millet, a language server. https://azdavis.net/posts/millet/

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

Note: I made Millet.

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

I’ve been working on a language server for Standard ML called Millet: https://azdavis.net/posts/millet/

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/

Hoping Millet doesn't mean anything offensive in any language… Studio Ghibli had this problem mildly with their film "Laputa" ("la puta" = "the whore" in Spanish).

There's https://github.com/standardml/smackage

It’s a group of mostly current/former CMU 15-150 TAs working on various SML tools, like:

https://github.com/brandonspark/mulligan

https://github.com/T-Brick/molasses

https://github.com/shwestrick/parse-sml

Just to make the MVP simpler.

I note in the caveats that the current approach is to recompute everything whenever even one file is changed. But that’s probably not sustainable, as I admit myself in https://azdavis.net/posts/pl-idea-tooling/ :

As an example, it would be unsustainable if, every time we changed a single function’s body, the language server had to re-typecheck the entire codebase. This might work for an initial proof-of-concept on a small codebase, but for large ones, the responsiveness of the language server would drop precipitously.

If I get around to addressing this, I’d probably use salsa and/or follow along this post: https://rust-analyzer.github.io//blog/2020/07/20/three-archi...

Author here, hope you like it!

You can enforce this with a clippy lint: https://rust-lang.github.io/rust-clippy/rust-1.62.0/index.ht...

https://azdavis.net/

I often write about programming languages.

Thanks!

Thanks! I updated it and replied to the parent comment.

Do you mean the inline code or code blocks? In any case, I tweaked the background to be more different from the page background (in both light and dark mode) and also gave inline code that same background. Does that help? https://github.com/azdavis/azdavis.net/commit/55199593abfb6e...

The definition I gave at the end of the article (the thing starting with `t ::=`) is basically a context-free grammar describing the syntax for terms of the calculus of constructions.

`t ::= ...` is saying "A CoC term, called t, can have the following forms ..." Then each case is separated by `|`.

The cases for application, abstraction, and forall are recursive, in that they contain t (or t') when the thing being defined is also called t. (The prime on t' is just to say that t and t' can be different terms.)

So for instance, the case for application is:

t(t')

That means if you already have two arbitrary CoC terms, called t and t', then if you write down first the term t, then a `(`, then the term t', then a `)`, then you've written down another CoC term representing the application of the term t to the term t'.

And the case for abstraction is

λ(x:t) t'

That means if you have two CoC terms t and t', then if you write down `λ`, then `(`, then a variable name (x is kind of a meta-variable-placeholder name, you can name the variable whatever you want), then `:`, then the term t, then `)`, then the term t', then you've written down an abstraction term. In this case, the variable x (or whatever you called it) has type t, and can appear free in t'.

Wow thanks! Never had my stuff shared out before to my knowledge but I appreciate it! I’ll take a look :D

Thank you!

Thank you! I’ve tried to make sure that my site reads well and loads fast, even on mobile.

There’s actually no JS on my site at load time, I run it all as a build step that transforms Markdown with inline LaTeX into pure HTML and CSS. https://github.com/azdavis/azdavis.net

I really appreciate your feedback, thank you!

interesting tangents

Yeah, I’ve found that explaining things by first giving an example and then generalizing often works better than trying to start with raw theory.

I actually wrote a bit about this on my website: https://azdavis.net/posts/lambda-cube/

I’ve been using my website as a way to practice writing, so please let me know what you think.

This is an old way of writing the type of parameters to a function. I believe the modern equivalent is

  char* combine(char* s, char* t) { ... }

Opinions differ on whether the * should be next to the type or next to the identifier. I prefer putting it next to the type.