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

21–30 of 39 posts

Re: CakeML – A Verified Implementation of ML

#21

Post by tempodox »

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…

I can't speak for others, but from a purely practical and non-academic point of view, I chose OCaml over SML because it's painless and easy to produce a standalone binary executable. Most SML implementations seem to be able to do that too, but require me to write compiler-specific glue code, IIRC. I don't want to have to dive into compiler internals to produce an executable. Also, I appreciate that the OCaml maintainers are not afraid to provide useful syntactic sugar although it may not seem “real FP”, like the `for` loop for instance. I seldom use the OO extension, but support for virtual methods can be very handy at times. You can implement the mechanics for those with functors too, but it's just more code to write that way.

Re: CakeML – A Verified Implementation of ML

#24

Post by more_original »

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)

Re: CakeML – A Verified Implementation of ML

#25

Post by gravypod »

clarus wrote: post #16
gravypod wrote: post #10

Go into the compiler explorer [0] and type the following val num = 10 Then take a look at the x86 generation. What is all of that. It doesn't look like executable data needed. Is that just implicit functions or something baked into the language? If it is, why isn't it being tree-shook?

It seems that there are some examples here: https://github.com/CakeML/cakeml/blob/master/explorer/exampl... Whould be cool to have these examples accessible from the web interface of the compiler explorer.

Sadly it doesn't seem like you can link to a compiler output from their compiler.

Re: CakeML – A Verified Implementation of ML

#26

Post by jetti »

DanielBMarkham wrote: post #3
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…

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.

Re: CakeML – A Verified Implementation of ML

#27

Post by nickpsecurity »

mafribe wrote: post #12
aisofteng wrote: post #9

Earlier quoted context omitted.

Could you expand on the significance of the first, for those of us not familiar with formal verification? Is this is a first because it is is theoretically difficult to do, or because it requires a lot of implementation time? What are some key points to read up and understand in order to properly appreciate this result, past the Wikipedia article on formal verification [1]? Thank you in advance for any elaboration. […

The problem with verifying realistic compilers is scale. We have known how to do it in principle since forever, and verification of toy compilers is part of textbooks on verification, such as [1], see also [2]. Realistic compilers are very complicated and Leroy's verification of CompCert took several man years for one of the world's leading compiler and verification guys. The purpose of research like CompCert and Cak…

No it goes further than that. They embedded assembly languages & many aspects of computation in HOL then built their compiler. The thing goes straight from logic to assembly with the theorem prover being the TCB outside the specs themselves. Whereas, CompCert was specified in Coq, would probably be extracted to an ML, and then that whole pile of code (hopefully verified to assembly) would do the job. Unless they're doing all the compiles in Coq itself w/ its checker. This is the part I could be really wrong on.

The TCB reduction is huge. Also, seL4 organization built the Simpl embedding of C in that to do "translation validation" (due to Jared Davis) of it straight to or matched against assembly. Skips the need for a CompCert-style, verified compiler altogether. Myreen et al's techniques were also used to verify theorem provers and now hardware.

So, the CakeML effort and its effects are huge. Maybe more so than CompCert given the flexibility & fact that it's a proprietary product now whereas Myreen et al's stuff is open. That's what I said back when I saw it. The prediction was confirmed as COGENT was built on the same technology with amazing results so far in cost of verification:

https://ts.data61.csiro.au/projects/TS/cogent.pml

Re: CakeML – A Verified Implementation of ML

#28

Post by nickpsecurity »

gravypod wrote: post #11
aisofteng wrote: post #9

Earlier quoted context omitted.

Could you expand on the significance of the first, for those of us not familiar with formal verification? Is this is a first because it is is theoretically difficult to do, or because it requires a lot of implementation time? What are some key points to read up and understand in order to properly appreciate this result, past the Wikipedia article on formal verification [1]? Thank you in advance for any elaboration. […

The problem with optimizing compilers is that you're changing what the user expects to come out. This is very dangerious because you need to be able to prove that what you've generated will work as the non-optimized version. I know of a few programs that when compiled with -O2 work fine but break with -O3. This is because some optimizations that are applied are just not what the programmer expected or in the older da…

Hence the Vellvm project and its ilk:

https://www.cis.upenn.edu/~stevez/vellvm

Re: CakeML – A Verified Implementation of ML

#29

Post by nickpsecurity »

Everyone with formal method background interested in this work should consider taking on one of their posted projects that would improve it. Especially Ocaml to CakeML translator.

https://cakeml.org/projects

Just email them first in case someone has done the work already. Academics sometimes are slow to update web sites due to digging deep into their research. ;) The best uses I can think of for CakeML are:

A reference implementation to do equivalence checks against with main language, a ML or not, being something optimized.

Someone to build other tools in that need high assurance of correctness. Prototype it to get the algorithm right using any amount of brains and tooling that already exist with an equivalent CakeML program coming out. Then, that turns into vetted object code.

A nice language for writing low-level interpreters, assemblers, or compilers that bootstrap others in a high-confidence way. Idea being in verifiable or reproducible builds where you want a starting point that can be verified by eye. They can look at the CakeML & assembly output with some extra assurance on top of hand-doing it. One might even use the incremental compilation paper on building up a Scheme to end up with a powerful, starting language plus assurance binary matches code.

Re: CakeML – A Verified Implementation of ML

#30

Post by nickpsecurity »

fmap wrote: post #7
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…

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 programs. Additionally, the Ocaml compiler was clean enough in architecture that Esterel was about to do source-to-object code validation required for its DO-178B-certified, code generator. They said they had to do way less work modifying or analyzing it than they expected. That means the Ocaml compiler itself might be a candidate for verification albeit probably a non-optimizing form of it. I'd also try the K framework that successfully handled the C semantics with KCC compiler. If it can handle C, I'd venture a guess that it should handle a better designed compiler and language. ;)

EDIT to add: Ocaml syntax is being worked on at link below.

https://github.com/CakeML/cakeml/tree/master/unverified/ocam...

Post reply on HN