> 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 lang

> 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?