I am really happy to have finally gotten a "hello world" from something compiled with Idris 2 (under Linux, to be clear) on the seL4 kernel. In theoretical terms, this was not much of a technical challenge, but it did take me a longer to achieve it than I'd expected because I wound up fighting CMake's assumptions a lot, so it felt very satisfying to finally get to that point.