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/

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

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

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!

Regarding Poly/ML (I'm quoting):

  * good performance and fantastic debugging tools
  * not merely “saving an image”, but sharable executable units, either including the Read-Eval-Print loop or standalone;
  * support for one hardware architecture after another (including Apple Silicon)
  * support for multi-threading (also here); they say that OCaml is finally catching up, 15 years later, thanks to having 100 times as much funding.

> A mystery I shall never understand is the difference in performance between SML/NJ and Poly/ML. The former enjoyed vastly greater funding and had a strong team of developers compared with DCJM’s one-man show. Benchmarks I ran for my ML book consistently gave SML/NJ a big performance advantage. But with Isabelle, the strong performer was Poly/ML. Once David got parallelism working, Poly/ML’s advantage was so overwhelming that we dropped our long-standing policy of supporting both compilers.

*another gem

These scripts are really limited. They only support the simplest .mlb files that are really just lists of other files, and the semantics are technically incorrect because they have no way to reset the environment when beginning each new .mlb file in, as the spec says they should. I use them scrappily during development and then generally use MLton for production builds. But you can get quite a lot done within those limitations, and it's very nice to have the faster compilation of Poly/ML, as well as the option of seeing error messages from more than one compiler.

That you can use CM as a library has always been really handy, but otherwise the same, using MLton for production builds.

MLton can do it's whole program optimization then output to LLVM which I believe should then be able to do auto-vectorization.

I don't have measurements to hand, but vaguely speaking, low. Low enough to be worth using for even quite modest calls into vector functions or optimised libraries.

> And can you pass SML function pointers into C code as callbacks?

Yes. At least, you can declare a function statically for export as a callback. You can't pass arbitrary function values.

You can call C/C++ from SML, and call SML from C/C++ from SML - though some neat potential uses are ruled out as MLton (unlike Poly/ML) doesn't support native threads and you can't call back from a different thread from the caller.

You can also compile to a library using MLton and use that from a C/C++ program - again only from a single thread, but it doesn't have to be the program's main thread.

Yeah, because OCaml has millions of lines of production code in many deployments (including Xen i.e. Amazon EC2) so it can't just break backward-compatibility to introduce multicore, nor can it afford to slow down existing code. These are constraints that the various MLs don't have :-)

While we're reminiscing, I imagine you also took Concepts in Programming Languages in second year (https://www.cl.cam.ac.uk/teaching/1011/ConceptsPL/ ?), which (after a tour de force through all sorts of paradigms that were consigned to the fossil record for the time being) did advertise Scala pretty heavily. I found that course to be a true gem and haven't seen anything like it at any of the other universities I've passed through since then.

Being hit with all that stuff from day one, fresh from a childhood of Spectrum Basic and Turbo Pascal, was a real shock to the system.

Still don't understand most of it to be honest, but it does still jar when I see the initialism used to mean Machine Learning.

Amen. I guarantee that Rust will regret not addressing this sooner. It's mature enough now that defining a semantics is more than appropriate.

If you want success within companies and not universities, then you need to treat the language as a product, serve the customer by investing time into documentation, guides, and branding just like with any product. I say this as a fan of ML languages, posts that complain about another language (OCaml) being more popular even though it is an inferior doesn't get new users.

[1]: I currently use F# daily but would be happy to switch to a variant of SML if it made sense.

You can do a lot with F#’s generics and interfaces.

There was. It was written by the author of this very submission and you can download it free from his site (follow the link trail from author's name at the bottom of the article). Great book, a real favourite, though I'm not sure it totally captures the anxiety-driven copy-paste frenzy of the true working programmer.

There is one SML compiler that has an extremely cute logo - SML# (https://smlsharp.github.io/en/)

“Branding Power” would be where given the choice between two products, the customer will choose the more expensive (or equally priced) product based solely on perception of brand quality or other brand characteristics. Think buying store brand vs buying name brand, an expensive name brand electronic item vs a cheap knock-off from a no-name Chinese manufacturer (the Chinese one might actually be better but that’s the point).

So not just a logo or cute drawings. It’s part of a more holistic experience, but especially the perception which is where logos and the like come into play. We engineers can stomp our feet but those are the rules of the game.

https://learn.microsoft.com/en-us/dotnet/core/deploying/nati...

Have I missed something? Because that page says pretty clearly that it's fully precompiled. It's not default, but it's an option

> The app will be available in the publish directory and will contain all the code needed to run in it, including a stripped-down version of the coreclr runtime.

Also check out the limitations section on the page. Some pretty big ones, including 'Limited diagnostic support (debugging and profiling).'

I see a big parallel between function to turn params into structs and accessors, both being mirrors of each others (cons/car/cdr as the root example) and the fact that a type definition encodes enough information to generate both at the semantic layer, with pattern matching as sugar.

So if any early LCF team member can shed some light if I'm imagining things or if LCF/ML were a rewrite of older recursive lisp practices into a cleaner formalism, I'd be glad.

ps: the fact that some LCF impl. were done in lisp also reinforces my belief.

An advantage of ML for theorem proving à la LCF is that you can use the type system to enforce some invariants ; namely you can prevent the user from ever building a value of type `theorem` that is not actually a valid theorem. I don't know how that would work in a dynamic language where you have access to everything.

I feel very lucky to have been in the right place at the right time, and ML’s structure was a pleasure then as it is now. The history of the language is indeed rather interesting.