The AdaOS Operating System (2000) | Hacker News Reader

The AdaOS Operating System (2000)

web.archive.org

87 pointsunilynx55 comments

The biggest issue with all of these "write a new operating system in my favorite language X" (where X is Ada, C, C++, D, Rust, etc) is that in almost all cases the operating system design slowly morphs into a buggy, half-baked version of an existing operating system. Rarely are there compelling new designs that are sufficiently better than what currently exists or was previously created in a different programming language.

While a different programming language can enable different levels of expressiveness, elegance, or nuance of control when interacting with hardware, ultimately it is the higher-level design concepts and design maturity that come into focus over time. (Does the design work in the real world? Is it "battle tested" and can address / overcome various failure modes?)

These forces have shaped the operating systems that we have today into what they are through years of heat and pressure. If you are contemplating writing a new operating system in your favorite language X, take a few years to study and understand how current operating systems solve real world problems and ask yourself how your ideas / designs will be as good as or better than what currently exists.

I think you are missing the point of what Ada can accomplish in contrast to other languages in terms of memory safety and criticality.

I personally think AdaOS is very compelling if you want a unique perspective on memory safety at such a large scale.

It's much more than a "favorite" language and certainly not even in the same realm of application as a language such as C.

Misra C in contrast to Ada, now that's a comparison. Not D, C++, etc.

I use Ada professionally and enjoy how expressive and powerful the language is in cleanly representing modular design and preventing errors. This is especially true with all of the features that came with Ada 2005 and Ada 2012.

I have no doubts about Ada or SPARK. I am questioning what is needed to make a new operating system design viable other than "it's written in Ada". What is needed to make an operating system that can be as good as or better than the POSIX-based operating systems that dominate computing.

>The biggest issue with all of these "write a new operating system in my favorite language X" (where X is Ada, C, C++, D, Rust, etc) is that in almost all cases the operating system design slowly morphs into a buggy, half-baked version of an existing operating system.

The whole point of writing a new OS in a language that prioritizes memory safety and provable correctness, like Ada or Rust, is specifically to explore the possibility that by using a better language, the OS won't morph into a buggy spaghetti code thing.

Safe languages impose fundamental constraints on the complexity of the system, that C/C++ and others do not, and eliminate entire classes of bugs and vulnerabilities at the compiler level.

People wonder why all our systems these days are insecure and getting hacked left and right. Provably correct software and compiler-enforced memory safety are two tools that will be part of the solution (maybe not sufficient, but absolutely necessary).

I agree that using a safe language is a necessity, especially for safety critical environments and to ensure better security. But a safe language alone does not ensure a good design. Ada is a great language (although strings are a bit of a pain), but that alone will not ensure a good operating system design.

POSIX is a great standard, but it is too tightly coupled with C. If a similarly mature and open Ada-based standard could be designed and created, that would be great. If such a design were created, what would it look like? How would files be represented and stored? How would you start, stop, or communicate with tasks? (POSIX-style signals? Rendezvous? Something else?)

There needs to be an open design that is as well thought out as the Ada programming language to really take advantage of everything that it offers.

There's an official Ada binding for POSIX.

Do you have a link to the documentation?

I am aware of Interfaces.C and the non-standard but highly-useful GNAT.OS_Lib. Any others would be nice to know about.

POSIX is a mature set of APIs and designs, but it is C-centric. It is an impedance mismatch discards many of the advantages of using Ada in the first place.

http://www.cs.fsu.edu/~baker/florist.html / http://sourceforge.net/projects/gnat-florist/

It's a standard.

(Was a standard, now withdrawn)

Well, with the exception of the BSD-like systems, none of the systems being written will actually run software people want to run unless they target those kernels. By definition, none of these kernels will therefore likely see widespread use. You can see a microcosm of this with Linux: popular commercial software like games often doesn't come to linux. To make an operating system that sees popular use, you'd likely need to emulate the API of an existing system.

This is actually fine. These systems aren't really trying to do that because they're created for other reasons. Maybe it is to learn about building operating systems and the author picked a not-C language? Maybe it is an academic research project like seL4 and the question being asked is "can we formally verify a whole kernel?" Maybe the kernel will use some esoteric feature of the processor, like i386's hardware threads or POWER's hypervisor? Maybe it is to produce a security kernel like GEMSOS or a separation kernel like Windriver's vxworks or Muen (which is written in Ada). Or it could be to build a different design of kernel, like a microkernel or unikernel. There are many reasons, and some of these are sold commercially and used in critical environments, albeit not on the scale of say Windows or Linux.

I don't think there's anything wrong with trying to build a kernel in a new language for many of the reasons other commenters have suggested. Perhaps it is simply to see if the language is suitable for kernel development? Maybe it is just to learn, and the developer in question picked their favourite language? I do agree with you though that doing some research is absolutely necessary. Writing a kernel is not a small project and it helps to decide what your aims are :)

You are exactly right! The "chicken and egg" problem is a large part of why these favorite language X operating systems slowly evolve into partial implementations of existing operating systems. What good is the favorite language X operating system if there is no software for it?

But wait a second, if the favorite language X operating system would implement these handful of POSIX APIs then look how much software could probably run with just a few tweaks. Except the POSIX APIs do not get implemented completely right. Or they suffer from terrible impedance mismatches due to the design differences or safe ideals that have to be relaxed in order to have them work. For example: Ada has unchecked conversion, unchecked deallocations, etc. Rust has unsafe.

A big part of the reason that GNU and Linux have succeeded is that they implemented Unix APIs with some innovations and improvements along the way.

Perhaps this is the crossover between Henry Spencer's observation about Unix ("Those who don't understand Unix are condemned to reinvent it, poorly.") and Greenspun's tenth rule ("Any sufficiently complicated C or Fortran program contains an ad-hoc, informally-specified, bug-ridden, slow implementation of half of Common Lisp.").

The crossover is: "Any sufficiently complicated, real-world operating system contains an ad-hoc, informally-specified, perhaps buggy, implementation of half of Unix."

Your post doesn't address the point that many of these "write a new operating system in my favorite language X" projects have great pedagogical value to the individual developing them. I've done plenty of experimentation in this area and I harbor no illusions that my efforts will ever be adopted into the mainstream. Operating-system development is an extremely broad and deep area of study. Writing toy operating-systems remains the best and most fulfilling way to learn.

While I can't speak for D, Rust, etc, I can speak for what Ada can offer the field. Ada, and especially its formally verifiable subset SPARK are languages designed with secure and maintainable development in mind. I think there's tremendous value in continuing research into the formal verification of operating-systems. SPARK is a much better option for this purpose than many of the other languages available.

Thank you for your work and research! We need an open design, formally-verifiable operating system that leverages what was learned in creating the research / toy operating systems to build an "industrial strength" operating system. A SPARK OS would be very nice indeed.

Thank you for the kind words! I can't take credit for breaking any real ground though. My experiments are quite small in scale!

I agree, formally verifiable operating-systems should really be the future. Take a look at Muen, they've done an amazing job at making a formally verified kernel in SPARK.

https://www.muen.sk/

I will check it out. Thank you!

I was just looking at this recently, funnily enough, while looking for other examples of x86 Operating-System development in Ada.

Here are a few other examples of Operating-System development in Ada, in various levels of completion.

- https://github.com/ajxs/cxos

- https://github.com/Lucretia/bare_bones

- https://marte.unican.es/todo.htm

- https://sourceforge.net/projects/lovelaceos/

- https://sourceforge.net/projects/sx-ada-kalinda/

Do not forget AuroraUX.

Back when it was based on OpenSolaris:

https://web.archive.org/web/20090314042407/http://auroraux.b... (Main Page)

https://web.archive.org/web/20090415214139/http://auroraux.b... (About)

Then DragonFlyBSD:

https://web.archive.org/web/20110824053558/http://www.aurora... (Main Page)

https://web.archive.org/web/20110824053558/http://www.aurora... (Why Ada?)

https://web.archive.org/web/20110904173302/http://www.aurora... (System Overview)

https://web.archive.org/web/20110904171806/http://www.aurora... (Project Goals)

https://web.archive.org/web/20091127065848/http://www.aurora... (Hydra Package Manager)

Thanks so much for the link! I'm having a little trouble finding the source on those pages. Is there a link to it that's still active?

Unfortunately not that I know of. :( I think I still have my hard drive somewhere back from 2009, I might be able to get some data off from it. It is an old Maxtor, 30 GB I think. The pins are broken so I will definitely have to fix that, but I will have to find it first.

I believe I can get in touch with someone who was really enthusiastic about the project! He was like 14 years old at the time, really really zealous so I would like to think that he made backups. I got the links above from him a couple of weeks (or months?) ago when we were going down the nostalgia lane. :) For what it is worth, I met him on IRC (freenode), in #ada.

I'm still lurking in there from time to time! If you can get it without too much trouble I'm sure there are a few people out there who will appreciate it!

I'm not sure how I forgot to mention this project, especially considering how high quality it is:

- https://www.muen.sk/

Muen is implemented in SPARK, and has been formally proven to contain no runtime errors, which is an incredible accomplishment.

- https://cs.uwaterloo.ca/~Brecht/courses/702/Possible-Reading... - for the Intel 432!

The Symbolics Lisp Machine could run Ada, of course.

And then there was the Rational/R1000s400, the first only and last "Ada-only" Computer.

http://datamuseum.dk/wiki/Rational/R1000s400

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

The R1000 was a workstation released in 1985 by Rational Software for the design, documentation, implementation, and maintenance of large software systems written using the Ada programming language. The R1000 featured an extensive tool set, including:

- an Ada-83-compatible program design language

- an integrated development environment that doubled as an operating system shell

- automatic generation of design documentation

- source-language debugging

- interactive design-rule checking and semantic analysis

- incremental compilation

- configuration management and version control.

Excerpts from Articles Filed Under: Rational 1000

http://www.somethinkodd.com/oddthinking/category/rat1000/

Rational 1000: A Time-Travelling Debugger with No Future

http://www.somethinkodd.com/oddthinking/2006/03/25/rational-...

https://sourceforge.net/projects/adaos/files/

Why is sourceforge's ui so bad? Why not display the files instead of expecting me to download some random zip file?

Sourceforge isn't a reputable website anymore. They have been known for bundling spyware/crapware with their installers of open source software.

That certainly happened, but as far as I can tell they stopped that years ago. It hurt their reputation immensely, though.

That was under previous owners. They've since been bought out by a company that actually gives a damn. Unfortunately there's a good argument for too little, too late. The damage to the brand's reputation is immense.

SF still has tons of ads and other really obnoxious UI choices. Take for example:

https://sourceforge.net/projects/pkgconfiglite/

There's so much crap on that page I couldn't even begin to care about. On the top half of the page: downloads this week, share this, open source software, business software, services, resources, sourceforge's twitter account, sourceforge's facebook account, sourceforge's linkedin, sourceforge newsletters, and of course a gigantic sourceforge banner.

If you go further: user reviews, recommended projects, top searches, other useful business software, similar business software, more twitter links unrelated to the project, related business categories.

SourceForge is a freaking dumpster fire even if they're no longer bundling malware.

That's what the owner of the project uploaded. Sourceforge allows you to host repositories like github/etc, but the repo of this project is empty: https://sourceforge.net/p/adaos/code/ref/master/

136.4KB is quite the tiny OS.

Any list of operating systems written in Ada should include Intel's first 32 bit OS iMAX:

https://cs.uwaterloo.ca/~Brecht/courses/702/Possible-Reading...

Does anyone know if the author completed other projects in Ada (or another language)? I'd be interested in reading some code as well as the specs.

Is Ada still around?

It never went anywhere, still used for what it was used...

A lot of flight and safety critical software has gone c++ at least in the US. Do178b approved g++ clones started popping up about 25 years ago and have made dramatic inroads.

>g++ clones

What does this mean? Something like certified forks of g++?

There have been those. Also there have been closed source compilers with identical switches. I have always suspected copyright violations because the scope of writing a c++ compiler but who knows.

What? I just left a job in defense software that used Ada and it was a fairly new program.

So we agree.

It never went anywhere => ie. it never left.

Still used for what it was used => ie. the same kind of software (defense, etc).

I also misread that as “never took off”.

The expression is "never went away" then, as "never went anywhere" usually means it dudded.

Interesting to hear that. DOD no longer requires ADA, so many projects that did use it have converted to C++. There were even people brought in to do automated Ada-> C++ conversion a number of years ago.

With the creation of the MISRA C standards for JSF these memory safety issues have largely been accounted for in the MISRA standards review process.

MISRA C definitely makes many improvements in this area. However, writing decent Ada code is so much easier than writing C code that conforms to MISRA ( or JSF ) standards.

There's a pretty good comparison here: https://learn.adacore.com/courses/SPARK_for_the_MISRA_C_Deve...

> ... C ....

> ... these memory safety issues have largely been accounted for ...

Hahaha. Hahahahahaha.

Instead of laughing like a child maybe provide a defendable argument?

Once again largely, C is a language not the compiler providing its implementation.

Yep. UB means that your program could crash, but it also means it's valid for the compiler to print out a warning and do the right thing, or error, or anything.

Yes. It's often used in safety-critical systems as an alternative to C, though C is still significantly more common.

Ada, Fortran, and even Cobol, satisfy the needs of a given domain: safety-critical environments for Ada, scientific computing for Fortran, business transactions for Cobol.

They won't be replaced in the next decades, and even some new systems might be implemented in them.

Languages for production were often designed to address a set of (hard) problems, as opposed to general-purpose languages (Python, Java, C++, etc.)

Sure, there are some web servers/apps written in Fortran or Ada. But those are examples of what the languages can achieve, not how they are actually used in production.

A Lot of older languages like ADA are still around, up to date and have surprisingly active and friendly communities. The health and state of any language should probably not be judged by how popular or how often it is mentioned on hacker news.

Yes. Latest language standard is Ada 2012.

Spark, a subset of Ada 2012 supports formal proofs of program properties ranging from absence of run-time errors to functional correctness (compliance of the code with formally specified requirements).

If you're curious, you can learn more at https://learn.adacore.com/courses/courses.html