3 ms·

Honestly, if I had the ambition to write an OS, I'd probably start by writing a new language.

by jesse__ 4y ago

AnimalMuppet 4y ago
There's historical precedent. But, what would be your design criteria for the new language?
- deleted 4y ago
  [deleted]
- jesse__ 4y ago
  > But, what would be your design criteria for the new language? I'd aim for somewhere between Rust and <other_imperitive_languages>. I'm certainly not qualified to speak with any authority on the matter of provably correct programs, but it seems to me there's a middle ground there that has yet to get a lot of attention. Something like C, but with markup describing data lifetimes, value ranges, permissible access, etc. The guys at Bungie did something similar for Destiny: https://www.youtube.com/watch?v=v2Q_zHG3vqg&t=2791s https://www.youtube.com/watch?v=v2Q_zHG3vqg&t=2791s There are also some PHd folks working on adding type annotations to C and restricting aliasing rules. Those annotations/rules get fed through a solver that proves it's free of latent memory bugs. As far as I remember they're trying to prove the Android thread scheduler. I couldn't find the talk/slides, but it turns out that's hard in C, but with a brand new language you could probably do it pretty easily (easily being a few man-years, instead of tens of).
  - thesuperbigfrog 4y ago
    >> I'd aim for somewhere between Rust and <other_imperitive_languages>. >> I'm certainly not qualified to speak with any authority on the matter of provably correct programs, but it seems to me there's a middle ground there that has yet to get a lot of attention. For "provably correct programs", the "<other_imperative_language>" could be SPARK: https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html https://learn.adacore.com/courses/intro-to-spark/chapters/01... If you wait a bit, Ferrocene may be what you are looking for: https://ferroussystems.com/ferrocene/ https://ferroussystems.com/ferrocene/

Honestly, if I had the ambition to write an OS, I'd probably start by writing a new language.

AnimalMuppet 4y ago

There's historical precedent. But, what would be your design criteria for the new language?

deleted 4y ago
[deleted]
jesse__ 4y ago
> But, what would be your design criteria for the new language? I'd aim for somewhere between Rust and <other_imperitive_languages>. I'm certainly not qualified to speak with any authority on the matter of provably correct programs, but it seems to me there's a middle ground there that has yet to get a lot of attention. Something like C, but with markup describing data lifetimes, value ranges, permissible access, etc. The guys at Bungie did something similar for Destiny: https://www.youtube.com/watch?v=v2Q_zHG3vqg&t=2791s https://www.youtube.com/watch?v=v2Q_zHG3vqg&t=2791s There are also some PHd folks working on adding type annotations to C and restricting aliasing rules. Those annotations/rules get fed through a solver that proves it's free of latent memory bugs. As far as I remember they're trying to prove the Android thread scheduler. I couldn't find the talk/slides, but it turns out that's hard in C, but with a brand new language you could probably do it pretty easily (easily being a few man-years, instead of tens of).
- thesuperbigfrog 4y ago
  >> I'd aim for somewhere between Rust and <other_imperitive_languages>. >> I'm certainly not qualified to speak with any authority on the matter of provably correct programs, but it seems to me there's a middle ground there that has yet to get a lot of attention. For "provably correct programs", the "<other_imperative_language>" could be SPARK: https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html https://learn.adacore.com/courses/intro-to-spark/chapters/01... If you wait a bit, Ferrocene may be what you are looking for: https://ferroussystems.com/ferrocene/ https://ferroussystems.com/ferrocene/