5 ms·

The Verified CakeML Compiler Back End [pdf]

39 points by ghettoimp 8y ago

ghettoimp 8y ago
Seriously amazing work. Formally verified compiler for a functional language down, with support for exceptions, GC, bignums, ... down to 5 different architectures, including x86 and ARM. Carried out in HOL4.
dang 8y ago
Recent thread: https://news.ycombinator.com/item?id=18493078 https://news.ycombinator.com/item?id=18493078
ncmncm 8y ago
What a waste that they did the work with an obligate-GC language and runtime. Without, it would be directly useful in making a verified OS and verified embedded systems. But Academia demands GC in any linguistic system, and systematically ignores all results that avoid it.
- xrchz 8y ago
  https://github.com/CakeML/cakeml/issues/111 https://github.com/CakeML/cakeml/issues/111
  - whitten 8y ago
    I read through the issue #111 you referenced. Both comments are from 2016, rather than any from this year. Perhaps you could reply and tell us the significance you see in this issue, and why it hasn't been addressed in at least two years.
- AgentOrange1234 8y ago
  While verified os/embedded systems would be great, is there not also value in trustworthy compilation of applications? A great deal of real software is written in java, python, js, swift, etc. ML may not be your cup of tea, but it’s a really nice language, and dismissing this as wasted work seems really harsh.
  - ncmncm 8y ago
    How much good do you get from proving an application program correct when it runs on an unreliable OS? I quite like the MLs, but would like to see a non-GC one.
- earthicus 8y ago
  The mlkit compiler [1] for Standard ML pioneered region based manual memory management, and was a primary design inspiration for Rust's memory system [2]. This research project (CakeML) has a different, and perfectly valid set of goals. [1] http://elsman.com/mlkit/ http://elsman.com/mlkit/ [2] https://doc.rust-lang.org/reference/influences.html https://doc.rust-lang.org/reference/influences.html
nickpsecurity 8y ago
I have some project ideas for people that build on this project: 1. Easy one is adding multiple forms of automated, test generation for CakeML. Then, an unverified-but-tested interpreter for it. So, one gets a Smalltalk-like development flow with safe-by-default language, easy testing, and certified compilation. https://cs.stanford.edu/people/saswat/research/ASTJSS.pdf https://cs.stanford.edu/people/saswat/research/ASTJSS.pdf 2. Moderately difficult to hard might be to extract the Stacklang and Wordlang parts as their own compiler targets. Right now, many target CompCert, which is proprietary. It would be better if they targeted totally-open, low-level languages. 3. Hard one might be to do a verified translator to LLVM intermediate code integrated with ALIVE checker or target QBE backend formalizing it in ALIVE fashion. QBE is designed to balance simplicity against optimization with an 80/20 rule for what optimizations are chosen. https://c9x.me/compile/ https://c9x.me/compile/ 4. Port affine types and/or a separation logic (esp with a solver) to CakeML to eliminate need for garbage collector. If not CakeML, then do it on low-level languages with ability to integrate them as trusted code into CakeML programs. 5. Port some kind of safe, concurrency model to it like Eiffel's SCOOP, Rust's, or Pony's. 6. Another easy project might be a CakeML to Ada, C, or Rust compiler like Tolmach's work doing the same for SML. Try K Framework if you want it easy with built-in tools. Runtime Verification Inc built a C semantics and static analyzer already. Gives something to work with. In any case, compiling to C lets you benefit from its optimizing compilers and verification tooling to simultaneously improve tuning/testing productivity and cost-effective bug hunting. https://web.cecs.pdx.edu/~apt/jfp98.ps https://web.cecs.pdx.edu/~apt/jfp98.ps 7. Hard, obvious project: extend CakeML itself with more features in ML-based or non-ML languages that will improve safety, productivity, maintainability, or performance (in that order or close to it). 8. Hard, obvious project: port more optimizations for functional programming from MLton, Haskell, or whatever projects might have useful ideas. Formally verify and empirically test them for correctness. http://www.mlton.org/References.attachments/060916-mlton.pdf http://www.mlton.org/References.attachments/060916-mlton.pdf
- earthicus 8y ago
  > Port affine types and/or a separation logic (esp with a solver) to CakeML to eliminate need for garbage collector. If not CakeML, then do it on low-level languages with ability to integrate them as trusted code into CakeML programs. I imagine you're aware of the mlkit compiler for sml. Do you know what would need to be done to glue mlkit code into cakeml in the way you're describing?

39 points by ghettoimp 8y ago

Seriously amazing work. Formally verified compiler for a functional language down, with support for exceptions, GC, bignums, ... down to 5 different architectures, including x86 and ARM. Carried out in HOL4.

dang 8y ago

Recent thread: https://news.ycombinator.com/item?id=18493078 https://news.ycombinator.com/item?id=18493078

ncmncm 8y ago

What a waste that they did the work with an obligate-GC language and runtime. Without, it would be directly useful in making a verified OS and verified embedded systems. But Academia demands GC in any linguistic system, and systematically ignores all results that avoid it.

xrchz 8y ago
https://github.com/CakeML/cakeml/issues/111 https://github.com/CakeML/cakeml/issues/111
- whitten 8y ago
  I read through the issue #111 you referenced. Both comments are from 2016, rather than any from this year. Perhaps you could reply and tell us the significance you see in this issue, and why it hasn't been addressed in at least two years.
AgentOrange1234 8y ago
While verified os/embedded systems would be great, is there not also value in trustworthy compilation of applications? A great deal of real software is written in java, python, js, swift, etc. ML may not be your cup of tea, but it’s a really nice language, and dismissing this as wasted work seems really harsh.
- ncmncm 8y ago
  How much good do you get from proving an application program correct when it runs on an unreliable OS? I quite like the MLs, but would like to see a non-GC one.
earthicus 8y ago
The mlkit compiler [1] for Standard ML pioneered region based manual memory management, and was a primary design inspiration for Rust's memory system [2]. This research project (CakeML) has a different, and perfectly valid set of goals. [1] http://elsman.com/mlkit/ http://elsman.com/mlkit/ [2] https://doc.rust-lang.org/reference/influences.html https://doc.rust-lang.org/reference/influences.html

nickpsecurity 8y ago

I have some project ideas for people that build on this project: 1. Easy one is adding multiple forms of automated, test generation for CakeML. Then, an unverified-but-tested interpreter for it. So, one gets a Smalltalk-like development flow with safe-by-default language, easy testing, and certified compilation. https://cs.stanford.edu/people/saswat/research/ASTJSS.pdf https://cs.stanford.edu/people/saswat/research/ASTJSS.pdf 2. Moderately difficult to hard might be to extract the Stacklang and Wordlang parts as their own compiler targets. Right now, many target CompCert, which is proprietary. It would be better if they targeted totally-open, low-level languages. 3. Hard one might be to do a verified translator to LLVM intermediate code integrated with ALIVE checker or target QBE backend formalizing it in ALIVE fashion. QBE is designed to balance simplicity against optimization with an 80/20 rule for what optimizations are chosen. https://c9x.me/compile/ https://c9x.me/compile/ 4. Port affine types and/or a separation logic (esp with a solver) to CakeML to eliminate need for garbage collector. If not CakeML, then do it on low-level languages with ability to integrate them as trusted code into CakeML programs. 5. Port some kind of safe, concurrency model to it like Eiffel's SCOOP, Rust's, or Pony's. 6. Another easy project might be a CakeML to Ada, C, or Rust compiler like Tolmach's work doing the same for SML. Try K Framework if you want it easy with built-in tools. Runtime Verification Inc built a C semantics and static analyzer already. Gives something to work with. In any case, compiling to C lets you benefit from its optimizing compilers and verification tooling to simultaneously improve tuning/testing productivity and cost-effective bug hunting. https://web.cecs.pdx.edu/~apt/jfp98.ps https://web.cecs.pdx.edu/~apt/jfp98.ps 7. Hard, obvious project: extend CakeML itself with more features in ML-based or non-ML languages that will improve safety, productivity, maintainability, or performance (in that order or close to it). 8. Hard, obvious project: port more optimizations for functional programming from MLton, Haskell, or whatever projects might have useful ideas. Formally verify and empirically test them for correctness. http://www.mlton.org/References.attachments/060916-mlton.pdf http://www.mlton.org/References.attachments/060916-mlton.pdf

earthicus 8y ago
> Port affine types and/or a separation logic (esp with a solver) to CakeML to eliminate need for garbage collector. If not CakeML, then do it on low-level languages with ability to integrate them as trusted code into CakeML programs. I imagine you're aware of the mlkit compiler for sml. Do you know what would need to be done to glue mlkit code into cakeml in the way you're describing?