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