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