Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The AdaOS Operating System (2000)

web.archive.org

Post reply on HN
Print view View original

41–50 of 56 posts

Re: The AdaOS Operating System (2000)

#41

Post by thesuperbigfrog »

SkyMarshal wrote: post #23
thesuperbigfrog wrote: post #14

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 lan…

>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…

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.

Re: The AdaOS Operating System (2000)

#42

Post by thesuperbigfrog »

zahllos wrote: post #26
thesuperbigfrog wrote: post #14

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 lan…

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 n…

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.

Re: The AdaOS Operating System (2000)

#43

Post by thesuperbigfrog »

ajxs wrote: post #28
thesuperbigfrog wrote: post #14

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 lan…

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-syste…

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.

Re: The AdaOS Operating System (2000)

#44

Post by thesuperbigfrog »

dapids wrote: post #21
thesuperbigfrog wrote: post #14

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 lan…

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 comp…

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.

Re: The AdaOS Operating System (2000)

#46

Post by ajxs »

ajxs wrote: post #27

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/project…

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.

Re: The AdaOS Operating System (2000)

#47

Post by ajxs »

thesuperbigfrog wrote: post #43
ajxs wrote: post #28

Earlier quoted context omitted.

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-syste…

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/

Re: The AdaOS Operating System (2000)

#48

Post by thesuperbigfrog »

thesuperbigfrog wrote: post #42
zahllos wrote: post #26

Earlier quoted context omitted.

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 n…

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…

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."

Re: The AdaOS Operating System (2000)

#49

Post by thesuperbigfrog »

ajxs wrote: post #47
thesuperbigfrog wrote: post #43

Earlier quoted context omitted.

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!

Re: The AdaOS Operating System (2000)

#50

Post by DonHopkins »

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-...

Post reply on HN