3 ms·

Thanks for the well-informed response. Sounds rather shallow to me, really. I can see the point in building a kernel in the safe subset of Rust, to provide str

Thanks for the well-informed response. Sounds rather shallow to me, really. I can see the point in building a kernel in the safe subset of Rust, to provide strong assurances about memory-management. I can see the point in building a kernel in SPARK to provide even stronger and more general assurances of correctness. I see the point in developing a kernel using a fully formal methodology, like Sel4. I can see the fun in hand-tuned kernels written in assembly, like KolibriOS. What's interesting about using a language with slightly different imperative building-blocks? Rust wouldn't be worth learning if it were merely C with different iterative statements. Or are there significant advantages to the various Oberons, that I'm unaware of?

cmrdporcupine 6y ago
If I understand it correctly, the primary purpose of the whole Oberon ecosystem is as an educational tool. And in that, I can see value. Having a holistic consistent system in one language/paradigm that you can build or analyze from the ground up has definite pedagogical value.
- Rochus 6y ago
  Right.
cedex12 6y ago
I'm no expert but it seemed to me the whole Pascal, Modula, Oberon story is in big part about Wirth chasing/exploring some optimal/balanced¹ programming language. So, it makes a lot of sense to have many variants and an evolution retracing both his learnings and opinions (that can change with time, and do, hopefully) and exploring different variations on a common theme. And developping an OS in any of these languages is pretty much a real-life test of their adequacy (meaning they are not just some vacuous formal exercise). Iirc, Wirth achieved some relatively lean but powerful languages at some point. Also, I don't understand your opposition to writing a kernel in some form of Oberon, but accepting pretty much any other language/paradigm ? ¹ Not that there is only _one_ optimal language.
- MaxBarraclough 6y ago
  > I don't understand your opposition to writing a kernel in some form of Oberon, but accepting pretty much any other language/paradigm When people talk about developing a kernel in a language other than C, the question that springs to mind is So what does this choice of language bring to the table? Rust and especially SPARK bring significant assurances of correctness, as they both improve greatly on the unsafety (supposing that's a word) of the C language. The same is true of a middle-of-the-road language like Java, but Java isn't ideally suited to kernel development. (If OS researchers prove me wrong on this point, then that's great, of course.) Assembly isn't a very compelling choice of language in terms of safety/correctness assurances, but I can see the appeal for a hobbyist OS, or for a carefully tuned high-performance codebase. From what I know of Oberon, using it for kernel development isn't in itself very interesting. Does it offer the guaranteed absence of broad categories of runtime errors? I guess it's still probably a rather safer language than C, and I presume its performance is ok, but this isn't anything new. (Of course, I've only talked about language. There are plenty of other ways an OS can be interesting besides the language it's implemented in, but that's the topic at hand.)
  - dmitriid 6y ago
    > The same is true of a middle-of-the-road language like Java, but Java isn't ideally suited to kernel development. (If OS researchers prove me wrong on this point, then that's great, of course.) Microsoft had an experimental OS called Singularity [1] --- start quote --- The lowest-level x86 interrupt dispatch code is written in assembly language and C. Once this code has done its job, it invokes the kernel, which runtime system and garbage collector are written in Sing# (an extended version of Spec#, itself an extension of C#) and runs in unprotected mode. --- end quote --- And don't forget that SIM cards in your phone run a Java... -ish [2,3] [1] https://en.wikipedia.org/wiki/Singularity_(operating_system) https://en.wikipedia.org/wiki/Singularity_(operating_system) [2] https://www.defcon.org/images/defcon-21/dc-21-presentations/Koscher-Butler/DEFCON-21-Koscher-Butler-The-Secret-Life-of-SIM-Cards-Updated.pdf https://www.defcon.org/images/defcon-21/dc-21-presentations/... [3] https://en.wikipedia.org/wiki/Java_Card https://en.wikipedia.org/wiki/Java_Card
microtherion 6y ago
I think you would be pretty hard pressed to design a system as functional and as clear as the Oberon System in so compact a manner that you can fit essentially all of it in one book (and implement it with a tiny team): https://people.inf.ethz.ch/wirth/ProjectOberon/index.html https://people.inf.ethz.ch/wirth/ProjectOberon/index.html I must admit I was a user of the system many years before I read the book, and I enjoyed reading the book considerably more than working with the system, but it's still a gem of a design. [Edited to fix link]
- cedex12 6y ago
  your link misses an `i` in `wirth`
  - microtherion 6y ago
    Thanks! I copied it from Prof Wrth's own homepage ;-)
i_don_t_know 6y ago
I think part of the argument is that if you want to have confidence in the correctness of a system, the system has to be so small and simple that anyone can fully understand it and keep it all in their head. For example, how do you know that the toolchains for Rust, Spark, sel4 work correctly? Have all aspects been verified or proven? Can a single person fully understand them? I’m not saying that’s the necessarily best criterion. The point is that all the guarantees that Rust, spark, Haskell, etc give are only meaningful if you can trust the tools to correctly implement them. Simplicity of the tools is one approach.
- MaxBarraclough 6y ago
  > how do you know that the toolchains for Rust, Spark, sel4 work correctly? Have all aspects been verified or proven In the case of Sel4, yes. The ARMv7 assembly code has been shown to be free of bugs. [0][1] SPARK Ada does not have a formally verified compiler, but there are various Ada compilers that are approved for use in life-and-death applications. The Boeing 777 flies on Ada code, for instance. [2] To my knowledge, compiler bugs aren't a major practical concern for SPARK, although a formally verified compiler would be a great addition. C has a fully verified compiler in CompCert. [3] I know of no other language with a fully verified compiler. (CompCert supports almost all C features, so it will either produce a valid binary for the input C code, or else fail with an error.) Rust has a bit of a history of troublesome compiler bugs. I think we're a way off seeing Rust used in critical systems, assuming it would even make sense to use a language like Rust. Memory management is handled quite differently in applications like avionics. > Can a single person fully understand them? The compilers/linkers? I imagine the most well-informed developers on the Rust and Ada compilers pretty much know how everything works, but really that's just a guess. If someone were to make a compiler specifically for SPARK, it could be simpler than a full Ada compiler, as SPARK forbids most Ada features. I don't know that this is likely to happen though. [0] https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html https://docs.sel4.systems/projects/sel4/frequently-asked-que... [1] https://sel4.systems/Info/FAQ/proof.pml https://sel4.systems/Info/FAQ/proof.pml [2] http://archive.adaic.com/projects/atwork/boeing.html http://archive.adaic.com/projects/atwork/boeing.html (This is about Ada, and is not specifically about the SPARK subset) [3] https://en.wikipedia.org/wiki/CompCert https://en.wikipedia.org/wiki/CompCert

cmrdporcupine 6y ago

If I understand it correctly, the primary purpose of the whole Oberon ecosystem is as an educational tool. And in that, I can see value. Having a holistic consistent system in one language/paradigm that you can build or analyze from the ground up has definite pedagogical value.

Rochus 6y ago
Right.

cedex12 6y ago

I'm no expert but it seemed to me the whole Pascal, Modula, Oberon story is in big part about Wirth chasing/exploring some optimal/balanced¹ programming language. So, it makes a lot of sense to have many variants and an evolution retracing both his learnings and opinions (that can change with time, and do, hopefully) and exploring different variations on a common theme. And developping an OS in any of these languages is pretty much a real-life test of their adequacy (meaning they are not just some vacuous formal exercise). Iirc, Wirth achieved some relatively lean but powerful languages at some point. Also, I don't understand your opposition to writing a kernel in some form of Oberon, but accepting pretty much any other language/paradigm ? ¹ Not that there is only _one_ optimal language.

MaxBarraclough 6y ago
> I don't understand your opposition to writing a kernel in some form of Oberon, but accepting pretty much any other language/paradigm When people talk about developing a kernel in a language other than C, the question that springs to mind is So what does this choice of language bring to the table? Rust and especially SPARK bring significant assurances of correctness, as they both improve greatly on the unsafety (supposing that's a word) of the C language. The same is true of a middle-of-the-road language like Java, but Java isn't ideally suited to kernel development. (If OS researchers prove me wrong on this point, then that's great, of course.) Assembly isn't a very compelling choice of language in terms of safety/correctness assurances, but I can see the appeal for a hobbyist OS, or for a carefully tuned high-performance codebase. From what I know of Oberon, using it for kernel development isn't in itself very interesting. Does it offer the guaranteed absence of broad categories of runtime errors? I guess it's still probably a rather safer language than C, and I presume its performance is ok, but this isn't anything new. (Of course, I've only talked about language. There are plenty of other ways an OS can be interesting besides the language it's implemented in, but that's the topic at hand.)
- dmitriid 6y ago
  > The same is true of a middle-of-the-road language like Java, but Java isn't ideally suited to kernel development. (If OS researchers prove me wrong on this point, then that's great, of course.) Microsoft had an experimental OS called Singularity [1] --- start quote --- The lowest-level x86 interrupt dispatch code is written in assembly language and C. Once this code has done its job, it invokes the kernel, which runtime system and garbage collector are written in Sing# (an extended version of Spec#, itself an extension of C#) and runs in unprotected mode. --- end quote --- And don't forget that SIM cards in your phone run a Java... -ish [2,3] [1] https://en.wikipedia.org/wiki/Singularity_(operating_system) https://en.wikipedia.org/wiki/Singularity_(operating_system) [2] https://www.defcon.org/images/defcon-21/dc-21-presentations/Koscher-Butler/DEFCON-21-Koscher-Butler-The-Secret-Life-of-SIM-Cards-Updated.pdf https://www.defcon.org/images/defcon-21/dc-21-presentations/... [3] https://en.wikipedia.org/wiki/Java_Card https://en.wikipedia.org/wiki/Java_Card

microtherion 6y ago

I think you would be pretty hard pressed to design a system as functional and as clear as the Oberon System in so compact a manner that you can fit essentially all of it in one book (and implement it with a tiny team): https://people.inf.ethz.ch/wirth/ProjectOberon/index.html https://people.inf.ethz.ch/wirth/ProjectOberon/index.html I must admit I was a user of the system many years before I read the book, and I enjoyed reading the book considerably more than working with the system, but it's still a gem of a design. [Edited to fix link]

cedex12 6y ago
your link misses an `i` in `wirth`
- microtherion 6y ago
  Thanks! I copied it from Prof Wrth's own homepage ;-)

i_don_t_know 6y ago

I think part of the argument is that if you want to have confidence in the correctness of a system, the system has to be so small and simple that anyone can fully understand it and keep it all in their head. For example, how do you know that the toolchains for Rust, Spark, sel4 work correctly? Have all aspects been verified or proven? Can a single person fully understand them? I’m not saying that’s the necessarily best criterion. The point is that all the guarantees that Rust, spark, Haskell, etc give are only meaningful if you can trust the tools to correctly implement them. Simplicity of the tools is one approach.

MaxBarraclough 6y ago
> how do you know that the toolchains for Rust, Spark, sel4 work correctly? Have all aspects been verified or proven In the case of Sel4, yes. The ARMv7 assembly code has been shown to be free of bugs. [0][1] SPARK Ada does not have a formally verified compiler, but there are various Ada compilers that are approved for use in life-and-death applications. The Boeing 777 flies on Ada code, for instance. [2] To my knowledge, compiler bugs aren't a major practical concern for SPARK, although a formally verified compiler would be a great addition. C has a fully verified compiler in CompCert. [3] I know of no other language with a fully verified compiler. (CompCert supports almost all C features, so it will either produce a valid binary for the input C code, or else fail with an error.) Rust has a bit of a history of troublesome compiler bugs. I think we're a way off seeing Rust used in critical systems, assuming it would even make sense to use a language like Rust. Memory management is handled quite differently in applications like avionics. > Can a single person fully understand them? The compilers/linkers? I imagine the most well-informed developers on the Rust and Ada compilers pretty much know how everything works, but really that's just a guess. If someone were to make a compiler specifically for SPARK, it could be simpler than a full Ada compiler, as SPARK forbids most Ada features. I don't know that this is likely to happen though. [0] https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html https://docs.sel4.systems/projects/sel4/frequently-asked-que... [1] https://sel4.systems/Info/FAQ/proof.pml https://sel4.systems/Info/FAQ/proof.pml [2] http://archive.adaic.com/projects/atwork/boeing.html http://archive.adaic.com/projects/atwork/boeing.html (This is about Ada, and is not specifically about the SPARK subset) [3] https://en.wikipedia.org/wiki/CompCert https://en.wikipedia.org/wiki/CompCert