1ML for non-specialists: introduction

[Here, ML means "Meta Language", not "Machine Learning". ML is used as an important building block inside some theorem provers and proof assistants]

The key thing with 1ML is that it merges the core and module system.

The ML family has historically had two systems: core and module. They are stratified in the sense they are separate languages. Modules can contain core expressions, but the other way around isn't possible.

1ML blends module and core. This means you have first-class modules in the core, which leads to a pretty nice language design.

Furthermore, this being Andreas Rossberg, the rigor at which this is carried out is very high. There's proofs of type safety and correctness along the way, generally to the same high bar as Standard ML (SML).

> communication barrier between academics who are in a position to discuss 1ML in depth and people who are in a position to write new compilers

I think there is s.th. wrong when people working on type systems can't write compilers.

1ML, not 1M

Title is "1ML for non-specialists: introduction".

From the article:

> 1ML is a type system designed by Andreas Rossberg and described in a ollection of papers by him