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.
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.
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.
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.
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.
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.
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.
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.
> 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?
Not a specialist in those things. Dont know functional programming. I do meta research to find opportunities for specialists to improve their work or create interesting work in the first place.
11 comments
[ 3.5 ms ] story [ 40.8 ms ] threadBut Academia demands GC in any linguistic system, and systematically ignores all results that avoid it.
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.
I quite like the MLs, but would like to see a non-GC one.
[1] http://elsman.com/mlkit/
[2] https://doc.rust-lang.org/reference/influences.html
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
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/
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
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
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?