Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

CakeML – A Verified Implementation of ML

cakeml.org

Post reply on HN
Print view View original

31–39 of 39 posts

Re: CakeML – A Verified Implementation of ML

#31

Post by vkuncak »

nickpsecurity wrote: post #30
fmap wrote: post #7

Earlier quoted context omitted.

I can add a few more data points. First regarding CakeML: - CakeML is written in HOL4, which is using ML. - SML, unlike Ocaml has a well-defined semantics and so there is a good starting point for a verified compiler. Second, regarding Ocaml, the easiest reason for choosing Ocaml over ML is because there is only one implementation of the language that everybody is using. This makes it a lot more likely that the ocaml…

On top of it, SML was literally designed to do proving. Writing provers, feeding algorithms into them, and later extracting algorithms out. Ocaml was designed as a practical language for software development. Unsurprisingly, the provers and verified tools tend to be done in SML or a subset of it while real-world software is done in Ocaml. That said, the CakeML team welcomes a translator for Ocaml that outputs CakeML…

It would be quite realistic and interesting to have a translation between the Scala subset that Leon project supports (leon.epfl.ch) and ML. A good starting point for this is Stainless, a redesigned version of Leon: https://github.com/epfl-lara/stainless

Re: CakeML – A Verified Implementation of ML

#32

Post by Athas »

larsberg wrote: post #17
Athas wrote: post #5

Earlier quoted context omitted.

I work with a bunch of people who were very involved in SML, and I've asked this question many times. They usually say that SML (as a language) stagnated because of personal conflicts in the standardisation committee. A bit of a "worse is better" microcosmos, really, with a focus on on discussing theoretical perfection instead of how to get things into the hands of users. You can partially see this in play today in t…

You can hear a bunch more about the full history of development of SML and interaction with OCaml here: https://www.youtube.com/watch?v=NVEgyJCTee4 I would definitely agree with the opinion above that the SML language designers fall in the camp of deliberating extensively and fully formalizing all new language features before considering them for inclusion. Today, there are two challenges right now in the Successor M…

> many of the implementation owners don't have a huge amount of time, so getting them to also agree to the new features is complicated.

That's another thing I noticed - people are not really prototyping the new ideas. I know that Bob Harper and John Reppy are also working on other projects, so they probably can't invest much implementation time on SML anymore. I wonder how OCaml and Haskell managed to keep implementers active.

The Successor-ML feature I'm just curious about is modular implicits (or some of the other alternatives mentioned by Harper). I much prefer the SML module system to Haskell's type classes, except that it is notationally more cumbersome in use. Sprinkling a little bit of implicit behaviour (when choice of functor is unambiguous) would help a lot.

Re: CakeML – A Verified Implementation of ML

#33

Post by rwmj »

vog wrote: post #2

I find it interesting that CakeML, like many other developments in this area, is based on SML (Standard ML) and not OCaml (Objective Caml). Moreover, whenever I read something about ML languages, it seems most people in the academic field talk about SML. Yet, it seems that OCaml is more popular among programmers and real-world projects. Even though these programmers come from the academic field, given the niche exist…

We use OCaml for the virt tools because it (a) generates efficient, standalone binaries and (b) lets us call out to C libraries really easily. We use OCaml over (say) C or C++ because it allows us to write code with far fewer bugs and headaches. You can find one of these large, real world OCaml programs here: https://github.com/libguestfs/libguestfs/tree/master/v2v

I think network effects do matter much more than you say. There is virtually no community around SML.

Re: CakeML – A Verified Implementation of ML

#34

Post by z1mm32m4n »

more_original wrote: post #24
Twirrim wrote: post #22

What is ML in this context? Neither CakeML nor Standard ML site appear to actually define it, and it's an acronym with a few definitions in tech (e.g. Machine Learning)

It's Meta Language. The ML language was developed in the early 1970s as a meta-language for the LCF theorem prover. ML was developed as a language for programming proof tactics. The strong type system and type soundness guarantees of ML were important to guarantee that such tactics could only prove correct theorems. https://en.wikipedia.org/wiki/ML_(programming_language)

For a bit of history about ML, see Appendix F: The Development of ML (on page 89) from here:

http://sml-family.org/sml97-defn.pdf

Re: CakeML – A Verified Implementation of ML

#36

Post by WorldMaker »

jetti wrote: post #26
DanielBMarkham wrote: post #3

Earlier quoted context omitted.

It may be similar to the reason for adoption for F# -- it does objects Doesn't matter if you actually code with objects. The important point for adoption is that it does them. So for a noob .NET programmer you say, hey, look at F#! You can code it just like C#. Kinda. But as soon as they start coding, you tell them nope, all of these types of things are actually antipatterns.

I disagree with your premise on why F# was adopted. It isn't because it does objects but it was really the first functional language that was pushed by Microsoft and ran on the .NET platform. Had F# not run on the CLR I don't think it would have nearly as many users as it does now.

That goes into why Microsoft (Research) chose to base F# on OCaml rather than SML (or Haskell, which Microsoft Research also has some fingers in that pie): it's not that useful targeting the CLR if you can't interact with other things running on the CLR (including the Base Class Library [BCL]). Presumably Microsoft could have have tried for something wild like trying to build a "CLR Object monad" for Haskell, but the F# team instead went with the existing, known commodity language family that already straddled that border between object systems and functional programming (OCaml).

Re: CakeML – A Verified Implementation of ML

#37

Post by larsberg »

Athas wrote: post #32
larsberg wrote: post #17

Earlier quoted context omitted.

You can hear a bunch more about the full history of development of SML and interaction with OCaml here: https://www.youtube.com/watch?v=NVEgyJCTee4 I would definitely agree with the opinion above that the SML language designers fall in the camp of deliberating extensively and fully formalizing all new language features before considering them for inclusion. Today, there are two challenges right now in the Successor M…

> many of the implementation owners don't have a huge amount of time, so getting them to also agree to the new features is complicated. That's another thing I noticed - people are not really prototyping the new ideas. I know that Bob Harper and John Reppy are also working on other projects, so they probably can't invest much implementation time on SML anymore. I wonder how OCaml and Haskell managed to keep implemente…

> I wonder how OCaml and Haskell managed to keep implementers active.

Members of that community could probably comment better than I, but it doesn't hurt that Microsoft Research supported two core Haskell team members and Inria has supported core OCaml work for most of the lifetimes of the projects. Their better corporate focus has also meant that as some fabulously enlightented BigCos took dependencies on them (most notably Standard Chartered for Haskell & Jane Street for OCaml), they've both hired core developers and supported the communities. I should add that these have been fantastic for the PL community in general and specifically ICFP funding & attendance!

For as much as the members of any one community might have differences of opinion with the choices of the others, success of any benefit us all. Even if we do grumble occasionally with the "can't get into ICFP this year unless you're in language {X}!" comments, where X was Scheme, then ML, then Haskell... :-)

> people are not really prototyping the new ideas

Yeah, John's group plus Matthew Fluet and a little bit of myself are trying to clean up Manticore enough to do a "final" release and journal paper, and that is kinda taking up a lot of our extra cycles. Several other folks have either retired or moved on to new areas (security, compiler verification, etc.).

I think that if we could find some places where the new ideas intersected with interesting novel (read: fundable) research topics, there'd be some additional energy into implementation work around them. Right now, certainly, stuff exists, at best, in private forks of (typically) MLton.

Re: CakeML – A Verified Implementation of ML

#38

Post by groovy2shoes »

nickpsecurity wrote: post #30
fmap wrote: post #7

Earlier quoted context omitted.

I can add a few more data points. First regarding CakeML: - CakeML is written in HOL4, which is using ML. - SML, unlike Ocaml has a well-defined semantics and so there is a good starting point for a verified compiler. Second, regarding Ocaml, the easiest reason for choosing Ocaml over ML is because there is only one implementation of the language that everybody is using. This makes it a lot more likely that the ocaml…

On top of it, SML was literally designed to do proving. Writing provers, feeding algorithms into them, and later extracting algorithms out. Ocaml was designed as a practical language for software development. Unsurprisingly, the provers and verified tools tend to be done in SML or a subset of it while real-world software is done in Ocaml. That said, the CakeML team welcomes a translator for Ocaml that outputs CakeML…

> SML was literally designed to do proving.

So was Caml (and its precursor Le-ML), originally :)

That it grew so far beyond that I think is a consequence of it not having a formal definition like SML. This allows the developers to extend the language willy-nilly without going through the grueling task of extending a formal semantics. On top of that, as another commentor pointed out, is the fact that there's a single "reference implementation", which means that users don't need to worry about getting locked-in when opting to use new functionality.

That said, SML is still a fantastic base for new research projects in the PL space, mostly for the very same reasons it hasn't seen nearly as much adoption in the "practical" space as Caml: it's a small, simple, well-understood, and formally-specified language that grants researchers an excellent starting point for their inquiries and experiments.

Re: CakeML – A Verified Implementation of ML

#39

Post by nickpsecurity »

groovy2shoes wrote: post #38
nickpsecurity wrote: post #30

Earlier quoted context omitted.

On top of it, SML was literally designed to do proving. Writing provers, feeding algorithms into them, and later extracting algorithms out. Ocaml was designed as a practical language for software development. Unsurprisingly, the provers and verified tools tend to be done in SML or a subset of it while real-world software is done in Ocaml. That said, the CakeML team welcomes a translator for Ocaml that outputs CakeML…

> SML was literally designed to do proving. So was Caml (and its precursor Le-ML), originally :) That it grew so far beyond that I think is a consequence of it not having a formal definition like SML. This allows the developers to extend the language willy-nilly without going through the grueling task of extending a formal semantics. On top of that, as another commentor pointed out, is the fact that there's a single…

Didnt know that about Caml. Neat. Perhaps a subset of Ocaml with formal semantics can do well, too.
Post reply on HN