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

11–20 of 39 posts

Re: CakeML – A Verified Implementation of ML

#11

Post by gravypod »

aisofteng wrote: post #9
mafribe wrote: post #6

Summary: CakeML is the first verified optimising compiler that bootstraps. Side note: Cake stands for CAmbridge KEnt, which is where (most of) CakeML's verification was carried out. The pioneering project in this space was X. Leroy's CompCert. This was the first verified optimising compiler. More precisely, a realistic, moderatly-optimising compiler for a large subset of the C language down to PowerPC and ARM assembl…

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 days just broken working code.

Formally verifying the output is difficult because you need to prove the same operation is happening both times even if they are extremely different in what they are doing. I'm assuming that's where the difficulty comes in.

Re: CakeML – A Verified Implementation of ML

#12

Post by mafribe »

aisofteng wrote: post #9
mafribe wrote: post #6

Summary: CakeML is the first verified optimising compiler that bootstraps. Side note: Cake stands for CAmbridge KEnt, which is where (most of) CakeML's verification was carried out. The pioneering project in this space was X. Leroy's CompCert. This was the first verified optimising compiler. More precisely, a realistic, moderatly-optimising compiler for a large subset of the C language down to PowerPC and ARM assembl…

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 CakeML is twofold:

- Provide a verified software toolchain for programmers with a minimal trusted computing base.

- Investigate how the cost (in a general sense) of formal verification in general and compiler verification in particular can be lowered, ideally to the point that normal programmers can routinely use formal verification.

The advance that CakeML makes over CompCert is bootstrapping: CakeML can compile itself, while CompCert (being a C compiler written in Ocaml) can't. Simplifying a bit, bootstrapping lowers the trusted computing base.

Maybe Leroy's [3, 4] are good starting point for learning about this field.

[1] T. Nipkow, G. Klein, Concrete Semantics. http://www.concrete-semantics.org/

[2] A. Chlipala, A verified compiler for an impure functional language. http://adam.chlipala.net/papers/ImpurePOPL10

[3] X. Leroy, Verifying a compiler: Why? How? How far? http://www.cgo.org/cgo2011/Xavier_Leroy.pdf

[4] X. Leroy, Formal verification of a realistic compiler. http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf

Re: CakeML – A Verified Implementation of ML

#13

Post by junke »

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 you need to add a semi-colon after the line (the AST was empty). A minimal program is simply "();", and compiles into something even more complex. A big part of it looks like runtime setup/cleanup code, common for all programs.

Re: CakeML – A Verified Implementation of ML

#14

Post by agumonkey »

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

The old ML compilers were more deeply rooted in academia. It was almost popular to write a new one to fiddle with a new idea (like concurrency). Performance and more pragmatic considerations were a bit secondary and that included OS interfaces. Caml had these, and thus was used to build some software somewhat popular on Unix systems (e.g. Unison, MLDonkey, a flash compiler). And while these days it might seem like we…

I wonder if the Objective part of it made it more lively in the mainstream eyes too instead of "stagnant/crude" sml.

Re: CakeML – A Verified Implementation of ML

#15

Post by aisofteng »

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…

Thank you.

Re: CakeML – A Verified Implementation of ML

#16

Post by clarus »

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.

Re: CakeML – A Verified Implementation of ML

#17

Post by larsberg »

Athas wrote: post #5
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 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 ML space:

- There's some broad agreement on a few things that should obviously be improved, but today 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. Life is way easier when you only have one implementation.

- There's a bunch of fantastic ideas (largely driven by Bob Harper) to integrate stuff like parallelism, cost model, etc. that will be fantastic for a next version of the language and specification. It's just a lot of work, and not really publishable, so it's mainly tenured faculty and "alumni" (like myself and probably the people you work with) driving it forward in our free time.

That said, I still love working on SML and its implementations (I mainly contribute to SML/NJ and Manticore) and it's a wonderful escape from the grim reality of quarterly goals and "get it out the door" release deadlines :-)

Re: CakeML – A Verified Implementation of ML

#18

Post by titanix2 »

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 think people wanting to use C# will stick to it, not learning another language to use it the same way as the one they already know.

The real value of objects in F# lies in the CLR compatibility. Access to the BCL and some existing code is a big advantage over OCaml for .neteers.

Re: CakeML – A Verified Implementation of ML

#19

Post by mhd »

agumonkey wrote: post #14
mhd wrote: post #4

Earlier quoted context omitted.

The old ML compilers were more deeply rooted in academia. It was almost popular to write a new one to fiddle with a new idea (like concurrency). Performance and more pragmatic considerations were a bit secondary and that included OS interfaces. Caml had these, and thus was used to build some software somewhat popular on Unix systems (e.g. Unison, MLDonkey, a flash compiler). And while these days it might seem like we…

I wonder if the Objective part of it made it more lively in the mainstream eyes too instead of "stagnant/crude" sml.

As far as I can remember, those were almost deprecated even way back when. It's never been much used for GUIs anyway, and I believe most servers and compilers were mostly written in a functional fashion.

Re: CakeML – A Verified Implementation of ML

#20

Post by agumonkey »

mhd wrote: post #19
agumonkey wrote: post #14

Earlier quoted context omitted.

I wonder if the Objective part of it made it more lively in the mainstream eyes too instead of "stagnant/crude" sml.

As far as I can remember, those were almost deprecated even way back when. It's never been much used for GUIs anyway, and I believe most servers and compilers were mostly written in a functional fashion.

Mystery stays intact.
Post reply on HN