Notes: 5th June 2026
A two week update this time, simply because last week and this things happened that meant I didn't make much progress on the things I want to write about here. Not bad things, just... Things :). PhD progress reviews, family visits, curriculum planning, that sort of thing. And it's still maybe a couple of weeks until I can really start focussing on the next Idris, but here we are.
Anyway. Progress continues on the latest experimental thing, which (I can't remember if I said anything about this...) is starting from scratch but intending to pull in all the good bits once I get going, and having case trees and local definitions as first class in the Idris core. I have some of the basic machinery up and running, so this week it's the evaluator. Having to deal with local definitions makes this a bit more complicated than before, but my plan is to deal with more of the complexity at this level, to reduce the number of horribly hacky ways we need in Idris 2 to deal with not having local definitions in the core and having to lift everything out, and manage scope appropriately in the elaborator. So, progress proceeds on that, as it does.
Also I got distracted by thinking a bit about other compilers and lightweight runtime systems, as I do occasionally. A couple of interesting things I looked at, without going into any more depth or commenting further here, are Lennart Augustsson's MicroHS which is based on combinators, and QBE which is a compiler backend that aims to be much more lightweight than, say, LLVM.