8 ms·

CakeML: A verified implementation of ML

53 points by poppingtonic 11y ago

nickpsecurity 11y ago
The best thing since FLINT. My scheme here was to piggy back on it by implementing fast, compatible DSL of CakeML in Racket or something. Do prototyping and testing with fast one. Once ready, compile functions with verified one. Works best for tools that will still have acceptable performance or run in batches overnight. Implement it on Verisoft stack if still available for down to CPU correctness. Also, some recent threads are on trustworthy compilers with verified vs reproducible builds. The ML languages have made robust compilers much easier to write. One can use this one for that to further reduce TCB and make compiler still easier to write vs C or whatever.
- e12e 11y ago
  > The best thing since FLINT. I assume you mean something related to?: http://flint.cs.yale.edu/flint/software.html http://flint.cs.yale.edu/flint/software.html I can't seem to find anything directly related to the software part - is SML/NJ a verified implementation of ML'97? I was exposed to a bit of Standard ML in university, and it always felt "nicer" than OCaml - but also less practical for actually getting anything done (probably because more people actually write real software in OCaml than in SML?). As for Racket and SML, I came across the following existing projects: "This is the Standard ML language embeded in PLT Scheme.": http://planet.racket-lang.org/display.ss?package=sml.plt&owner=chongkai http://planet.racket-lang.org/display.ss?package=sml.plt&own... "A Standard ML to Racket Translator without type inferencing and checking": https://github.com/stslxg/sml-racket https://github.com/stslxg/sml-racket And while I like the concept of Racket (I've yet to play with it as much as I think it deserves), why not simply use SML/NJ or MLTON if CakeML is a subset of SML? Or possibly implement a non-verfied implementation either on top of MLTON/SML/NJ, or in ML? Curious about your line of thinking there.
  - nickpsecurity 11y ago
    "I can't seem to find anything directly related to the software part - is SML/NJ a verified implementation of ML'97?" The page says it's included in SML/NJ distribution. Probably one of the tarballs. SML/NJ is just an old compiler for SML 1997. FLINT is techniques and code needed to certify compilation. They're different things but apparently bundled. "probably because more people actually write real software in OCaml than in SML?)" That's what I've gathered. The SML people have strong academic focus with Ocaml people having more practical focus. A big community built up around it. "As for Racket and SML, I came across" That's neat but they both have no type checking. I'll skip to next question as it's relevant here. " Curious about your line of thinking there." LISP is easy to parse, easy to interpret, has robust compilers, supports incremental compilation of individual functions, modify/debug a running program, and especially extension with macros. Racket is a batteries-included LISP with IDE, active community, and strong support for DSL's. Now, ML's strengths are strong typing, type inference, easily integrated into formal verification, lots of prior work/tools in that (incl compilers), and easy to model w/ macros. Embedding ML in a LISP gives me the best of both worlds. I once did this in a 4GL to have rapid development with extraction to C/C++ with safety, portability, etc stuff auto-inserted. Easy parsing also lets you extract to a number of ML's or LISP's to use their tooling to catch extra errors in yours. I've only run into two tools outside of Racket doing this sort of thing: https://github.com/combinatorylogic/mbase https://github.com/combinatorylogic/mbase http://julialang.org/ http://julialang.org/ Mbase is used in commercial tools for static analysis, etc. It's a LISP and toolset custom designed for easily making things like compilers that comes with many DSL's for specific tasks, including ML. Julia raises the bar for 3GL language experience via a compiler written in LISP (femtolisp) that immediately translates the AST's into LISP expressions and works from there. It's more advanced than, but similar advantages to, the 4GL I wrote as it combines best properties of static typing, dynamic productivity, macros, and C support. Underlying LISP that enables that is only about 1,000loc to implement IIRC. So, that's my thinking. I also thought of implementing the tool in MLton, too, but such things are even easier when your tooling and language makes extractions trivial. ;)
julian_1 11y ago
Awesome. If anyone knows about this project - how easy would would it be to re-target the backend code generator for something other than x86 or ARM?
- sanxiyn 11y ago
  It's reasonably retargetable. If you look under compiler/targets in the repository, you will find MIPS and RISC-V backends.
vosper 11y ago
> A long-term goal is to make proof assistants into trustworthy and practical program development and implementation platforms. The CakeML compiler verification is an example of proof-assistant-based development; specifically, of proven-correct synthesis of machine code from higher-order logic specifications. Is CakeML intended to be used to make things, or is it more of a proof of concept?
- gillygize 11y ago
  "practical program development" implies that it is intended to make things and is not just proof of concept, no?
  - vosper 11y ago
    I read it as they're talking about making proof assistants practical one day, and CakeML is a step on the road to that goal. If they then move onto the next step, where does that leave CakeML?
- poppingtonic 11y ago
  One of the research organizations using CakeML is MIRI (Machine Intelligence Research Institute), which is doing research in machine self-reference. They recently used HOL, an automated theorem prover, to demonstrate a formal correspondence between the model of HOL within HOL (“inner HOL”) and HOL itself (“outer HOL”). Informally speaking, Fallenstein and Kumar show that one can always build an interpretation of terms in inner HOL such that they have the same meaning as terms in outer HOL. The authors then show that if statements of a certain kind are provable in HOL’s model of itself, they are true in (outer) HOL. See more here: https://intelligence.org/2015/12/04/new-paper-proof-producing-reflection-for-hol/ https://intelligence.org/2015/12/04/new-paper-proof-producin...
Ericson2314 11y ago
I'm sorry, but why do people still use HOL? It seems so much more annoying than type-theoretic approaches (Coq/Agda/Idris/Lean). [Cool work judging from the title nevertheless.]
- nickpsecurity 11y ago
  I remember they used to say it was a sound and strong logic vs others.
  - Ericson2314 11y ago
    I've never heard of any soundness issues with the PLs I've mentioned. As to "strength" you mean expressiveness? At the very least the type theoretic ones give one the same expressive power with less redundancy.
    - nickpsecurity 11y ago
      I read it in comments on forums where people argued about one prover vs another. I can't find an academic source with Google talking about it. No worries then.
- adrianN 11y ago
  Different strokes for different folks.
  - Ericson2314 11y ago
    I suppose so...
- mafribe 11y ago
  HOL is a classical rather than constructive logic. Moreover, there is less concern about soundness of the logic.
  - Ericson2314 11y ago

53 points by poppingtonic 11y ago

The best thing since FLINT. My scheme here was to piggy back on it by implementing fast, compatible DSL of CakeML in Racket or something. Do prototyping and testing with fast one. Once ready, compile functions with verified one. Works best for tools that will still have acceptable performance or run in batches overnight. Implement it on Verisoft stack if still available for down to CPU correctness. Also, some recent threads are on trustworthy compilers with verified vs reproducible builds. The ML languages have made robust compilers much easier to write. One can use this one for that to further reduce TCB and make compiler still easier to write vs C or whatever.

e12e 11y ago
> The best thing since FLINT. I assume you mean something related to?: http://flint.cs.yale.edu/flint/software.html http://flint.cs.yale.edu/flint/software.html I can't seem to find anything directly related to the software part - is SML/NJ a verified implementation of ML'97? I was exposed to a bit of Standard ML in university, and it always felt "nicer" than OCaml - but also less practical for actually getting anything done (probably because more people actually write real software in OCaml than in SML?). As for Racket and SML, I came across the following existing projects: "This is the Standard ML language embeded in PLT Scheme.": http://planet.racket-lang.org/display.ss?package=sml.plt&owner=chongkai http://planet.racket-lang.org/display.ss?package=sml.plt&own... "A Standard ML to Racket Translator without type inferencing and checking": https://github.com/stslxg/sml-racket https://github.com/stslxg/sml-racket And while I like the concept of Racket (I've yet to play with it as much as I think it deserves), why not simply use SML/NJ or MLTON if CakeML is a subset of SML? Or possibly implement a non-verfied implementation either on top of MLTON/SML/NJ, or in ML? Curious about your line of thinking there.
- nickpsecurity 11y ago
  "I can't seem to find anything directly related to the software part - is SML/NJ a verified implementation of ML'97?" The page says it's included in SML/NJ distribution. Probably one of the tarballs. SML/NJ is just an old compiler for SML 1997. FLINT is techniques and code needed to certify compilation. They're different things but apparently bundled. "probably because more people actually write real software in OCaml than in SML?)" That's what I've gathered. The SML people have strong academic focus with Ocaml people having more practical focus. A big community built up around it. "As for Racket and SML, I came across" That's neat but they both have no type checking. I'll skip to next question as it's relevant here. " Curious about your line of thinking there." LISP is easy to parse, easy to interpret, has robust compilers, supports incremental compilation of individual functions, modify/debug a running program, and especially extension with macros. Racket is a batteries-included LISP with IDE, active community, and strong support for DSL's. Now, ML's strengths are strong typing, type inference, easily integrated into formal verification, lots of prior work/tools in that (incl compilers), and easy to model w/ macros. Embedding ML in a LISP gives me the best of both worlds. I once did this in a 4GL to have rapid development with extraction to C/C++ with safety, portability, etc stuff auto-inserted. Easy parsing also lets you extract to a number of ML's or LISP's to use their tooling to catch extra errors in yours. I've only run into two tools outside of Racket doing this sort of thing: https://github.com/combinatorylogic/mbase https://github.com/combinatorylogic/mbase http://julialang.org/ http://julialang.org/ Mbase is used in commercial tools for static analysis, etc. It's a LISP and toolset custom designed for easily making things like compilers that comes with many DSL's for specific tasks, including ML. Julia raises the bar for 3GL language experience via a compiler written in LISP (femtolisp) that immediately translates the AST's into LISP expressions and works from there. It's more advanced than, but similar advantages to, the 4GL I wrote as it combines best properties of static typing, dynamic productivity, macros, and C support. Underlying LISP that enables that is only about 1,000loc to implement IIRC. So, that's my thinking. I also thought of implementing the tool in MLton, too, but such things are even easier when your tooling and language makes extractions trivial. ;)

julian_1 11y ago

Awesome. If anyone knows about this project - how easy would would it be to re-target the backend code generator for something other than x86 or ARM?

sanxiyn 11y ago
It's reasonably retargetable. If you look under compiler/targets in the repository, you will find MIPS and RISC-V backends.

vosper 11y ago

> A long-term goal is to make proof assistants into trustworthy and practical program development and implementation platforms. The CakeML compiler verification is an example of proof-assistant-based development; specifically, of proven-correct synthesis of machine code from higher-order logic specifications. Is CakeML intended to be used to make things, or is it more of a proof of concept?

gillygize 11y ago
"practical program development" implies that it is intended to make things and is not just proof of concept, no?
- vosper 11y ago
  I read it as they're talking about making proof assistants practical one day, and CakeML is a step on the road to that goal. If they then move onto the next step, where does that leave CakeML?
poppingtonic 11y ago
One of the research organizations using CakeML is MIRI (Machine Intelligence Research Institute), which is doing research in machine self-reference. They recently used HOL, an automated theorem prover, to demonstrate a formal correspondence between the model of HOL within HOL (“inner HOL”) and HOL itself (“outer HOL”). Informally speaking, Fallenstein and Kumar show that one can always build an interpretation of terms in inner HOL such that they have the same meaning as terms in outer HOL. The authors then show that if statements of a certain kind are provable in HOL’s model of itself, they are true in (outer) HOL. See more here: https://intelligence.org/2015/12/04/new-paper-proof-producing-reflection-for-hol/ https://intelligence.org/2015/12/04/new-paper-proof-producin...

Ericson2314 11y ago

I'm sorry, but why do people still use HOL? It seems so much more annoying than type-theoretic approaches (Coq/Agda/Idris/Lean). [Cool work judging from the title nevertheless.]

nickpsecurity 11y ago
I remember they used to say it was a sound and strong logic vs others.
- Ericson2314 11y ago
  I've never heard of any soundness issues with the PLs I've mentioned. As to "strength" you mean expressiveness? At the very least the type theoretic ones give one the same expressive power with less redundancy.
  - nickpsecurity 11y ago
    I read it in comments on forums where people argued about one prover vs another. I can't find an academic source with Google talking about it. No worries then.
adrianN 11y ago
Different strokes for different folks.
- Ericson2314 11y ago
  I suppose so...
mafribe 11y ago
HOL is a classical rather than constructive logic. Moreover, there is less concern about soundness of the logic.
- Ericson2314 11y ago