Comment by nickpsecurity

2 years ago

OS’s written in Ada included MaRTE OS (open source), Intel’s BiiN system, and the Army Secure Operating System (ASOS) (IIRC).

The Muen Seperation Kernel (muen.sk) is a secure hypervisor written in SPARK Ada.

Ada was designed for low-level programming. It makes sense it does operating systems fairly easily. Parts of them will break its safety features. They can be validated with external tools, though.

Another trick, used in House with H layer, is to wrap the lowest-level parts which you might do in assembly. Build the GC or whatever, too. Then, everything else is in the higher-level language. These data, the lowest-level portions can be specified, verified, and implemented.

Fair point.

I was slightly more getting at it being not a natural fit for a Unix-like OS but I accept your point.

AFAIK, sadly, Intel BiiN is lost to history now. A Register reader wrote in to me to tell me that he was one of the developers.

  • That's cool that you heard from one.

    What I really wanted from a developer was the i960. Specifically, the version with the object protections. That might be worth buying today for secure, embedded work. If I found the right person, I'd ask them to open-source, or at least dual-license, the i960. For embedded systems, leave it as a RISC-V alternative or port it to RISC-V.

    • > That's cool that you heard from one.

      It was. (If you ever see this, thank you again, Mr Buchanan.)

      > What I really wanted from a developer was the i960.

      Interesting choice!

      Given that Intel has a number of distinctive architectures in its historical portfolio, and is in trouble these days due to the competition from Arm and perhaps even RISC-V, I would love to see it do either experimental revivals of some of its architectures, or open up the specs for other ones.

      (Someone there must bitterly regret selling off its Arm architecture license cheaply to Marvell; now, Marvell is worth more than Intel itself.)

      How about modern die-shrinks of i860 and i960, or even just FPGA versions?

      After the DEC/Compaq/HP implosion, Intel also ended owning the Alpha. I would not be at all averse to a resurrected Alpha chip, even if a very low-end chip on some old cheaper process tech.

      3 replies →