The Verified CakeML Compiler Back End [pdf]
cs.cmu.edu
cs.cmu.edu
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.
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?
But 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.