I guess you are the author of linked paper. Well done.

I wonder if you have any opinions on how useful higher-kinded types (HKTs), one of the most requested features for Rust, would have been in implementing this OS. For example the absence of HKTs means that Rust can't have smooth and general handling of monads that is comparable to Haskell's. Would Haskell-style monads or Arrows have been helpful?

Thanks.

I believe HKT would have been useful but am not really sure how much HKT would have helped me overall. They would likely have been most useful (if at all) in the VFS/S5FS/VM stages that I was unable to fully get to.

Honestly, I have not used haskell enough to definitively say whether monads/arrows would have been useful.

I guess the only way to find out is to await the emergence of low-level languages with HKTs and then run suitable experiments.

Ah, so all memory used by the kernel must be listed in sections loaded by the bootloader? As opposed to the normal situation where the kernel just starts grabbing it from the hardware?

I know no specifics of the situation, but llvm optimisations can be manually toggled through rustc. Maybe there are more special-case optimisations that could help.