Show HN: Dragon Microkernel in Spark Ada

github.com

4 points·tigerlang··2 comments

Hello,

I am currently actively developing the “Dragon” microkernel. However, what sets it apart from Linux and other kernels is, of course, its microkernel architecture, and secondly, the fact that it is written and verified using SPARK Ada (gnatprove).

But that doesn’t mean kernel services have to be written only in SPARK Ada; I added the C SDK so that anyone can write a service. The only downside is that this service isn’t the most secure compared to a gnatprove-verified kernel, but the microkernel architecture makes up for it.

I think the main reason I'm developing this microkernel is to create a proven kernel that can be used in some way on user machines, not just on high-security systems.

Dragon is currently in a early stage of development.

If you like this idea, I'd ask you to take a look at the source code (if you know it) or at the C SDK. The current version is 0.4 (we're close to releasing version 0.5, which will include bug fixes and C SDK documentation).

Consider using a metaobject system and having every object/type in your system able to use ASN.1 -- this will allow any language to hook into this system and you get OpenVMS-like interlanguage compatibility "for free". Add in a stream system and a general text <-> object system and you now have a system where every program is using a system-provided parser for command parameters.

Reply on news.ycombinator.com