Discussion
RE: https://mastodon.gamedev.place/@aeva/116925130760988827
there's another better world where those who jump ship from Linux distributions and the Linux Kernel project start contributing to and using Ironclad/Gloire/muenSK
yes, this is an Ada+SPARK post. :cereal_killer:
@theruran I was pretty interested in Muen and Ada/SPARK, but I found a CLAUDE.md in an AdaCore repository and took it as a red flag. You seem more clued in than I am, though, so: what's your read on the situation regarding Ada and LLM use?
@lykso yeah, fuck AdaCore. they are an unfortunate and problematic sole benefactor of the community.
@theruran Doesn't that situation feel kind of worrisome? I was considering doing an seL4 and Idris combo, myself.
@lykso I've compared muenSK and seL4, and architecturally I would go with seL4. I don't like seL4's verification process because it uses C with a separate proof assistant, but at least it's complete and well-reviewed and described.
In my opinion, muenSK needs more ISA support, and to copy seL4's capability-based architecture, with stronger, more complete proofs. it needs contributors. 
@lykso the Ada community needs a bootstrappable compiler, that at least can bootstrap GNAT, but ideally be a full implementation with better compiler engineering. ideally it includes a SPARK proof verifier.
we are all too old to have the time and energy to do this. I doubt it would be funded. instead, the young software engineers are spending their cycles on JavaScript and Rust. (just look at how that is going.)
@lykso what I would want to do, is at least make SPARK-verified bindings to seL4's C APIs. then MicroKit's.
@theruran Certainly sounds like an interesting project!
Idris is technically bootstrappable from C already, though there is a step in which roughly 10k lines of Chez Scheme are generated from the Idris source code. Still, analyzing that much code seems more easily done than bootstrapping an alternative Ada compiler, and I don't know of anything about the core team that might cause problems. It's a younger language, but this also means there's less institutional inertia to worry about.
I don't believe the software engineering field, such as it is, can even save itself. I only see self-destruction ahead.
and if you're wondering what I mean, software engineering is still lagging on systems engineering, systems architecture, systems security, systems assurance, systems resilience (and all the other "-ilities"), as well as formal verification which is in their own field (!)
as long as software firms lack systems engineering leadership, they will never dig themselves out of their deep pits of technical debt.
imagined other: damn.. pretty bleak, theruran.
me: whoops sorry posting again
Install bonfire.cafe
Get the full app experience
