CakeML – A Verified Implementation of ML | Hacker News Reader

CakeML – A Verified Implementation of ML

cakeml.org

99 pointstosh24 comments

The example implementation of Unix cat(1) is... intimidating!

https://github.com/CakeML/cakeml/blob/master/examples/iocatP...

It is possible I am misunderstanding something, but I am pretty sure that is not cat(1) implemented in CakeML. It is an implementation of cat(1) verified using the same HOL libraries, tactics, etc. that they used to verify the implementation of CakeML. I didn't look closely enough to see if they have gone all the way and reimplemented HOL inside of CakeML.

If I recall correctly, most CakeML code is actually written in HOL4 and then translated down to CakeML, and compiled to machine code from there. Unfortunately there isn't very much in the way of documentation or examples for writing concrete CakeML, as the developers seem to use it more as an intermediate representation.

Edit: The page describes two frontends. The first is a "proof-producing synthesis" of a CakeML AST from "ML-like functions in HOL". This is what I believe is the more typical use case of CakeML. The second frontend is a more traditional frontend which parse concrete CakeML syntax.

Where do people usually use Standard ML type languages? What are these most suitable for? (Please excuse me for a lame question. I am an amateur.)

In my undergrad, SML was the language used to teach functional programming concepts.

Plenty of research is happening, which is why SML has a wide variety of variant interpreters and compilers, all adhering (mostly) to the standard core. ConcurrentML is an interesting paradigm, and MLTon made some good strides into full-program optimization.

But most of that is academic, and OCaml really stole most of the thunder (by being small and fast, despite having more syntactic warts -- and no, making things look like JS ain't a solution to that).

As an aside: The ML-ML/MachineLearning and JS-JavaScript/Jane Street interpretations makes comments on anything even tangentially related harder to parse. Reason coming in and closing the loop has not made this easier. I wonder whether this affects anyone else.

I'm affected by the "ML" switcheroo, but Jane Street isn't big enough on my monitor to cause confusion.

And thankfully there's little cause for "NLP" ambiguity these days.

> And thankfully there's little cause for "NLP" ambiguity these days.

Is there not? When I Google "NLP" the first results are for "Neuro-Linguistic Programming", which I assume is NOT the definition you'd consider the important one. The fact that it also has "programming" in the name and has to do with "linguistics" does not make things easier.

True, but its popularity seems to have decreased enough that I don't get that many quackery-NLP news in my personal bubble / here. So when NLP does turn up, it usually means the right thing.

That people now use "ML" when it's just a simple matter of NLP is another matter…

A good example of this is ML Kit from google [0] vs MLKit a ML compiler [1]

[0]: https://developers.google.com/ml-kit/

[1]: http://www.elsman.com/mlkit/

Doubly confusing as people associate "Kit" names with Apple a lot of the time - a company and platform that has nothing to do with either project.

One reason is probably, that it's a small language with a fully specified semantics. Also, despite its age, it is still a modern language. It's had features like lambdas, type inference, algebraic data types, generics, modules, etc. for decades.

One area people tend to use ML-based languages is software that makes heavy use of algebraic/inductive datatypes, e.g., compilers and interactive theorem provers. (Implementing a theorem prover was the original motivation for ML.) That said, the ML family is general-purpose and suitable for many tasks.

OCAML has this area more than SML does, however.

I don't think that's clear.

- HOL4, Isabelle, ProofPower : Standard ML

- Coq, HOL Light, HOL Zero : OCaml

- Lean : C++

- Agda, Idris: Haskell

- Mizar : Pascal

- Metamath : C

Whenever this comes up, the answer seems to be "for programming language research and proofs in academia" and not much else.

It's a pity. SML is in many ways a joy to work with. The language doesn't change, which is a nice thing in itself in the current climate, but it has many things people still look for in modern languages (type inference, pattern matching, a module system). Multiple compliant compilers are available that produce fast code. The syntax is delightful, relying on neither brace delimiters nor syntactic whitespace. The language and Basis library are small enough that a developer can realistically aim to learn the whole thing. It is a comfortably idiomatic general-purpose functional language: lacking object or procedural syntax but relaxed about side-effects and occasional use of mutable types.

There are problems. Everyone will have their own list of things they expect a language to have, that SML lacks (mine: a map container in the standard library; record updating without rebinding all the elements individually; universal printf/toString, no matter how hacky). There is no standard foreign-function interface for calling native libraries, and no standard memory model - each compiler has its own. There is no standard build system (though I dunno, maybe this is a good thing). Libraries are sorely lacking, although those written many years ago usually still work. Because the language is a stem for academic developments, there are several variations that are intriguing but not actually compatible - CakeML seems to be an example, as it doesn't support functors or records.

I find SML pretty nice for writing small command-line utilities - like a functional alternative to Go or Python.

> It's a pity. SML is in many ways a joy to work with. The language doesn't change, which is a nice thing in itself in the current climate, but it has many things people still look for in modern languages (type inference, pattern matching, a module system). Multiple compliant compilers are available that produce fast code. The syntax is delightful, relying on neither brace delimiters nor syntactic whitespace.

is it now ? Caml has been taught for a long time to a lot of to-be engineering students in france, and it was frankly almost universally hated ; likewise for people that are taught LISP.

> is it now ?

Well of course I think so, since I said it... But -

> Caml has been taught for a long time to a lot of to-be engineering students in france, and it was frankly almost universally hated

It's possible to wonder why a language like SML doesn't get more use outside academia, since so many people have been taught it as students. And it seems a reasonable explanation that many people who were taught these languages simply disliked the experience. If you're forced to learn a weird non-procedural language with no obvious application and a super-picky type checker that you can't understand, why would you like it?

I had a vaguely similar experience myself, when taught SML as a student in the 90s. I enjoyed it as an exercise, but by the end of the course I still didn't have any useful intuition for how to write a whole program in it. Meanwhile over on the C++ course, the object/procedural mix seemed to make more obvious sense as a way to structure things.

Now, after years working in C++, I think of SML as the easier language and in many ways more natural.

Not sure about SML but its close cousin OCaml (which I learned after SML) is used a lot in industry by some big names:

* Facebook - OCaml for Hack, Reason, Flow - static analysis and compilers

* Jane Street - heavy user for their entire backend

* Bloomberg

* Citrix

etc https://ocaml.org/learn/companies.html

Haskell is also closely related but different as it has lazy evaluation unlike SML

https://wiki.haskell.org/Haskell_in_industry

I was taught SML as a first year CS student to learn the basics of programming (although I had already used C-like languages). ML stands for Meta Language - it was originally designed and used to prove theorems. That's why SML itself tends to be quite an academic thing to this day.

Education, primarily * . It is the simplest in the family that includes Rust, Haskell, Scala, OCaml, Swift, F#, Elm, etc. So it makes an excellent environment for learning the foundational concepts of this family. In particular, you can find your ground first before you're forced to reckon with implicits (Scala) type classes/traits (Haskell, Rust, Scala), macros (Rust), etc.

I do some sporadic, long-term work on Ponyo [0] to provide a base for exploration. I've also got a WIP "ebook" [1] on Standard ML.

* Although it's also used for prototyping. A lot of Google and Facebook projects were prototyped in SML or OCaml such as React, Reason, certain WASM components, etc.

[0] https://github.com/eatonphil/ponyo

[1] http://ponyo.org/guides

It isn't simpler than Elm, although that's probably a good thing, because Elm is missing some features that are definitely worth learning.

For me, SML was the gateway drug that lead me to OCaml.

Online SML (SMLNJ): https://www.tutorialspoint.com/execute_smlnj_online.php

I really liked SMLNJ plus there's MLTON which is a highly optimizing SML compiler, albeit not so friendly with error messages (or it wasn't when I used it).

Reply on news.ycombinator.com