CakeML – A Verified Implementation of ML

by tosh • 8 years ago

99 24 8 years ago

varshithr• 8 years ago

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

asib• 8 years ago

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

mhd3• 8 years ago

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

superlopuh• 8 years ago

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.

lower• 8 years ago

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.

xrchz2• 8 years ago

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.

seanmcdirmid• 8 years ago

OCAML has this area more than SML does, however.

cannam3• 8 years ago

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.

jcelerier• 8 years ago

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.

isomorph• 8 years ago

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.

eatonphil• 8 years ago

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

giornogiovanna• 8 years ago

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

geoalchimista• 8 years ago

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

pinewurst• 8 years ago

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

frou_dh• 8 years ago

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

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

trurl• 8 years ago

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.

Gajurgensen• 8 years ago

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.

CakeML – A Verified Implementation of ML

Related Stories