| HN Mirror

Fascinatingly, the more you post, the less convinced I am that Ada could ever be suitable for this use case. I looked at all these links to see what's been done:

Muen: If I am reading the allocator in https://git.codelabs.ch/?p=muen.git;a=tree;f=tools/liballoc/... correctly, it simply has no deallocator function at all. It does have a "Clear" function, but there's no sign that it has any ability to statically check that calling it is safe. That is exactly what we're talking about.

Nvidia: No public source code, and it's not obvious what actually exists here, beyond a compiler to Nvidia hardware.

Genode: This project is mostly written in C++. There is a very tiny, experimental amount of Ada in it (< 400 lines of code). There's certainly nothing that speaks to the questions discussed in this thread (safe dynamic allocation/deallocation, security, etc.).

ApexAda: This is a marketing brochure. Also this marketing brochure talks about "significant deployments in satellite communications, avionics, weapons control systems, and a myriad of other mil/aero applications," all of which - as discussed elsewhere in these comment - are applications that neither need nor want dynamic allocation (and are generally not exposed to deeply-structured untrusted input, for that matter).

Green Hills: This looks interesting - there's a POSIX filesystem and a UDP socket implementation, both of which (probably) want dynamic memory allocation. That is, at last, an application that needs dynamic allocation. Is it actually written in Ada? I see that the RTOS itself supports development in C, C++, and Ada, and they claim to offer a BSD socket implementation, so they at least have C bindings. I don't see any claim about what language it's written in, and Green Hills seems to do a lot of C work (see e.g. https://www.ghs.com/products/micro_velosity.html). If it's in Ada, then I think this gets the closest to what would be needed for the Linux kernel - do you know how their filesystem and socket implementations handle dynamic allocation? (I'll also note that they lost their certification many years ago, so if the answer is that they have safe code because they spent a whole lot of time perfecting a single version of an OS, then that's a very different problem space from Linux, which is constantly changing.)

Wind River: This is a marketing page without much detail, but it looks like it's a hypervisor to run general-purpose OSes on top of, not a general-purpose OS itself, which means it probably does not need dynamic memory allocation, or that if it does, the safety of deallocation can be verified by hand.

---

No Ada developer has done what's being done in this patchset, and it's pretty insulting to the folks putting in the work to claim it's been done and Gish-gallop a bunch of random links and expect people to put in the time to figure out what exactly you're claiming already exists. Everyone knows it's possible to write code in Ada. Nobody is asking if Ada can be used for completely unrelated purposes. You may as well link to GORILLAS.BAS and ask why the Linux kernel isn't using QBasic, a memory-safe language if you use the subset without PEEK and POKE.

Write - or point to - a kernel driver for a UNIX-like operating system written in Ada, that safely handles dynamic allocation. That's the clear bright-line goal. If you think that's not the right goal, say why.