Ironclad OS project popping out Unix-like kernel in a unique mix of languages

If you're looking for a Unix-like, POSIX-compatible, real-time kernel, there's no shortage of projects trying to build one. Ironclad stands out for using the Ada programming language and its formally verifiable SPARK subset. The Ironclad OS project is writing a new Unix-like OS kernel, aimed at small-footprint and embedded …

[elDog]

Oh, goody! I can put Ada back on my resume.

I think I remember intentionally removing it since it made me look old (which wasn't really necessary), and since hiring types would get a befuddled look on their faces when encountering that word.

Never really got to use Ada in a real production environment. Some difficult coding exercises around handling communication buffers, etc. Gov't mandated Ada for new IT projects but it really wasn't ready at the time. One fall-back was to use JOVIAL (which also doesn't show up on my resume.)

[Anonymous Coward]

Re: Oh, goody! I can put Ada back on my resume.

With Github telling us how Typescript is surging, because of how it's strong typing is better for AI, my first thought was: "Typescript good. Ada better"

I propose leaning into this with AI extensions and a new language AIDA.

(You may send grateful donations in the meme-coin of your choice)

[Brave Coward]

'A new language AIDA'

Veni, vidi, Verdi?

[ICL1900-G3]

Re: 'A new language AIDA'

Brilliant. Have a beer on me!

[Anonymous Coward]

Re: 'A new language AIDA'

Actually, AIDA was replaced by DIANA (as an intermediate language) for ADA. This must have been a while back, as I remember reading the DIANA spec for my final year project in the late 80s. See Wikipedia for a brief mention of DIANA.

[martinusher]

Re: Oh, goody! I can put Ada back on my resume.

Nothing wrong with ADA, it just suffered a bit from over specification -- people demand that a language does everything and anything out of the box and start niping when it doesn't happen. (Algol suffered the same fate -- Algol68 promised a lot but only really delivered a subset like the RRE's compiler, a fine effort that was eminently usable but just not good enough for the purists.)

[Alan J. Wylie]

PERQ / Accent / Mach

Back around 1980, I briefly evaluated an ICL PERQ workstation, running PNX (yes, really!). It could run several other operating systems, including Accent, which was a predecessor of Mach.

Wikipedia articles: PERQ, Accent

[ICL1900-G3]

Re: PERQ / Accent / Mach

I lusted after a Perq when they came out. For its time, hugely capable.

[Doctor Syntax]

Not at all Unix-like but the UCSD pSystem (the original Apple Pascal) was written in Pascal. The OS, application and P-code interpreter all had to live in a small address space, enabling it to run on a 6502 or Z80. (As a L1 cache any self-respecting modern core would turn its nose up at the size of the memory available on the box I had it running on.)

[DS999]

Why does this

Read like a DoD project to me? Their home page doesn't look like it, but the implementation of MAC and especially use of Ada sure do!

Other than Apple using seL4 as the kernel in the Secure Element, is there any use of formal verification in any mass market products? Who will use this if the defense industry doesn't?

[Doctor Syntax]

Re: Why does this

"Who will use this if the defense industry doesn't?"

If it has the backing to ensure it keeps going (and that might need defence use) then all those capital equipment makers that are currently leaving users stranded on obsolete versions of Windows ought to turn to it.

[Roland6]

Re: Why does this

The main user of ADA is the defense establishment.

[kevlar700]

Re: Why does this

Nvidia have shipped something like a billion cores with it already and announced expanding on their use recently at defcon 33. I also use it in a tiny startup for products we will soon ship.

https://www.adacore.com/papers/nvidia-adoption-of-spark-new-era-in-security-critical-software-development

[elsergiovolador]

AMOS

Just make Unix in AMOS Basic.

[42656e4d203239]

Re: AMOS

>>in AMOS Basic.

Like the multi-user pacman with invisible ghosts?

If you get that specific reference you probably know who I am (or at least who I worked with/for)

/beer cos not everyone knows about AMOS Basic --->

[DarkwavePunk]

Re: AMOS

I had its bastard cousin STOS for the Atari ST because I'm a peasant. Have beer, the idea tickled me and brought back fond memories.

[that one in the corner]

Re: AMOS

Wasn't AMOS the bastard cousin of STOS rather than t'other way around? To the extent that AMOS generally didn't really play nice with anything else on the Amiga (UI consistency etc)? Not that that probably mattered much to the intended audience.

[Ross 12]

Re: AMOS

Yeah STOS was the original, then the Amoeba games machine wanted in on the action

[DarkwavePunk]

Re: AMOS

You seem to be correct. I just always felt like a pleb for having an ST.

[Julz]

What

Comes around, goes around.

Came here to spout some nostalgia of projects past but it seems like I'm late to the party.

[David Newall]

"The only other formally verified kernel we're aware of is the seL4 microkernel"

Formally verified, as in TCSEC (a.k.a. DoD Orange book) A division system.

https://en.wikipedia.org/wiki/Trusted_Computer_System_Evaluation_Criteria:

Examples of A1-class systems are Honeywell's SCOMP, Aesec's GEMSOS, and Boeing's SNS Server. Two that were unevaluated were the production LOCK platform and the cancelled DEC VAX Security Kernel.

[Liam Proven]

> Formally verified, as in TCSEC

...?

No. That's a very different sort of verification. The "formal" part denotes a sort of mathematical proof:

en.wikipedia.org/wiki/Formal_verification

[MarkMLl]

Wirth not involved?

> Although the late great Niklaus "Bucky" Wirth wasn't directly involved, Ada's syntax – and its strong typing - are visibly inspired by Pascal.

At least some of the ALGOL-68 "Minority Report" authors were involved in the early days.

"The European community was especially responsive, particularly valuable since language research had been more active there than in the United States over the previous decade. ONR London paid several academics (Dijkstra, Hoare, Wirth, ...) to provide inputs, but we got more valuable aid from European industry." -- http://archive.adaic.com/pol-hist/history/holwg-93/holwg-93.htm

In practice it owes more to ALGOL-68 and Modula-2 than to Pascal.

[Roland6]

“Possibly thanks to riding on Rust's coat-tails, Ada … getting more attention…”

The big advantage ADA has over Rust is that it is formally defined and has well established quality tool chains that don’t change every few months.

I suggest. Having looked at Rust, people look around and find Ada is a more attractive proposition. The only problem Ada has is that it’s not “new” and “trendy”, it then neither is Rust really given the hype around Vibe.

[kevlar700]

Ada SPARK is Ace

Gloire Musl/Ironclad also runs on x86 and runs the mate desktop environment.

Nvidia have also written Drive OS recently in fornally verified Ada SPARK.

There have also been one or two other formally verified kernels written in Ada SPARK recently but for low level embedded. HiRTOS is one.

I chose Ada over Rust a few years ago when I switched from embedded C and desktop Go to Ada SPARK (mostly just to bronze level) and now I want to use Ada SPARK for everything. It hurts a little when I have to read C or Dart now (Dart libs can be nice such as bcrypt or horridly elaborate oop like cbor).