5 ms·

Wouldn't it make more sense to use a much more mature safety-centric language with a proper language spec like Ada?

oxnrtr 5y ago
No.
mustache_kimono 5y ago
Ada maybe isn't very well adapted to kernel code? From what I know of Ada, doesn't it get it's memory safety from either a GC or not freeing memory entirely? That is -- ownership rules are pretty new to Ada/SPARK. C-style syntax and community interest also favor Rust. This spec argument has always seemed like a red-herring to me. Can you explain why the Ada spec would be a significant factor in this instance?
- modshatereality 5y ago
  It's always fun to read peoples drive-by opinions about the only decent language IMO. Ada is highly compatible with C code. For dynamic allocations with "ownership" there is the concept of memory pools which CAN use a GC if thats how you choose to implement the pool allocator.
  - mustache_kimono 5y ago
    Haha, I'm sorry if it seemed like I ever knew what I was talking about. I thought asking questions would make it clear that I don't. Remain interested in the potential advantages of Ada compared to Rust for Linux kernel development, if you would care to point me in the right direction.
- NextHendrix 5y ago
  >Ada maybe isn't very well adapted to kernel code? From what I know of Ada, doesn't it get it's memory safety from either a GC or not freeing memory entirely? That is -- ownership rules are pretty new to Ada/SPARK. I think GC is optional with Ada, as far as I know the memory safety comes from raising exceptions (or refusing to compile) when it detects memory-unsafe operations (array bounds checking etc). >C-style syntax and community interest also favor Rust. That's fair, C-like languages are instantly familiar with software people and rust seems to have a more hip image than old man fuddy-duddy Ada. >This spec argument has always seemed like a red-herring to me. Can you explain why the Ada spec would be a significant factor in this instance? I'm not arguing for Ada over Rust (I'm not a software guy) so I don't mean it as a red herring, but wouldn't a suite of static verification tools and a formally verified compiler require a spec to be tested against?
  - mustache_kimono 5y ago
    Re: spec, not if the spec is implementation (and project's values) defined. I mean -- the Rust project has a ridiculous # of tests which define language behavior without having an ISO standard. Yes, implementation defined behavior in C is usually a place where C compiler engineers trade safety for speed. Yes, that's usually a bad trade. However, I'd look at this situation re: Rust vs. C in a different way though -- the Rust project's values are why defining a standard is less important. I think a spec is often a red herring because a bunch of folks living in the slum of C, when asked if they would all like to move into Rust's nice 3 bedroom by the park, instead always seem to ask: Wouldn't it be better to form a committee about building us a cathedral? Ada might be better. Someone should try it, but until then I'll take Rust.
throwaway894345 5y ago
Honestly if Ada hasn't caught on in the intervening 30 years (despite a lengthy government issued monopoly) then it probably isn't a good choice. A more mature Rust would be nice, but it's gravy at this point.
ahupp 5y ago
(caveat: I've read a bit about Ada but don't have any deep familiarity with it) Ada is safe compared to the other languages of its day, but I'm not sure it compares favorably with Rust. IIRC it does have more of a focus on safe arithmetic rather than memory safety.
- FabienC 5y ago
  The focus of Ada is not on safe arithmetic only, it's on functional safety at large: the code does what it is specified to do and nothing else. Ada shines in its specification power, how developers can express what the code is supposed to do (strong typing, ranges, contracts, invariants, generics, etc.). And then you can either check your code at "compile time" with SPARK [1], that provides a mathematical proof that you code follows the specification. SPARK also proves that you don't have buffer overflows or division by zero for instance. Or you can have checks inserted in the run-time code which greatly improves the benefits of testing as every deviation from specifications will be detected, not only the ones you decided to check in your tests. In terms of memory safety, Ada always had an edge on C/C++ because of the lower usage of pointers (see parameter modes [2]) and the emphasis on stack allocation. Now with the introduction of ownership in SPARK it's getting on par with Rust on that topic. [1] https://learn.adacore.com/courses/intro-to-spark/chapters/05_Proof_Of_Functional_Correctness.html#advanced-contracts https://learn.adacore.com/courses/intro-to-spark/chapters/05... [2] https://learn.adacore.com/courses/intro-to-ada/chapters/subprograms.html#parameter-modes https://learn.adacore.com/courses/intro-to-ada/chapters/subp...
  - quotemstr 5y ago
    Interesting. I wasn't aware that safety in Ada had developed to this point. Maybe I'll have to take another look at the language!
m463 5y ago
I remember writing Ada (long ago) and my take was: it's nice to work on existing Ada code, but I thought it was tedious to write new code. there was also a lot of unchecked conversion under the hood. (disclaimer: I haven't really paid attention to newer versions of Ada)

No.

Ada maybe isn't very well adapted to kernel code? From what I know of Ada, doesn't it get it's memory safety from either a GC or not freeing memory entirely? That is -- ownership rules are pretty new to Ada/SPARK. C-style syntax and community interest also favor Rust. This spec argument has always seemed like a red-herring to me. Can you explain why the Ada spec would be a significant factor in this instance?

modshatereality 5y ago
It's always fun to read peoples drive-by opinions about the only decent language IMO. Ada is highly compatible with C code. For dynamic allocations with "ownership" there is the concept of memory pools which CAN use a GC if thats how you choose to implement the pool allocator.
- mustache_kimono 5y ago
  Haha, I'm sorry if it seemed like I ever knew what I was talking about. I thought asking questions would make it clear that I don't. Remain interested in the potential advantages of Ada compared to Rust for Linux kernel development, if you would care to point me in the right direction.
NextHendrix 5y ago
>Ada maybe isn't very well adapted to kernel code? From what I know of Ada, doesn't it get it's memory safety from either a GC or not freeing memory entirely? That is -- ownership rules are pretty new to Ada/SPARK. I think GC is optional with Ada, as far as I know the memory safety comes from raising exceptions (or refusing to compile) when it detects memory-unsafe operations (array bounds checking etc). >C-style syntax and community interest also favor Rust. That's fair, C-like languages are instantly familiar with software people and rust seems to have a more hip image than old man fuddy-duddy Ada. >This spec argument has always seemed like a red-herring to me. Can you explain why the Ada spec would be a significant factor in this instance? I'm not arguing for Ada over Rust (I'm not a software guy) so I don't mean it as a red herring, but wouldn't a suite of static verification tools and a formally verified compiler require a spec to be tested against?
- mustache_kimono 5y ago
  Re: spec, not if the spec is implementation (and project's values) defined. I mean -- the Rust project has a ridiculous # of tests which define language behavior without having an ISO standard. Yes, implementation defined behavior in C is usually a place where C compiler engineers trade safety for speed. Yes, that's usually a bad trade. However, I'd look at this situation re: Rust vs. C in a different way though -- the Rust project's values are why defining a standard is less important. I think a spec is often a red herring because a bunch of folks living in the slum of C, when asked if they would all like to move into Rust's nice 3 bedroom by the park, instead always seem to ask: Wouldn't it be better to form a committee about building us a cathedral? Ada might be better. Someone should try it, but until then I'll take Rust.

throwaway894345 5y ago

Honestly if Ada hasn't caught on in the intervening 30 years (despite a lengthy government issued monopoly) then it probably isn't a good choice. A more mature Rust would be nice, but it's gravy at this point.

ahupp 5y ago

(caveat: I've read a bit about Ada but don't have any deep familiarity with it) Ada is safe compared to the other languages of its day, but I'm not sure it compares favorably with Rust. IIRC it does have more of a focus on safe arithmetic rather than memory safety.

FabienC 5y ago
The focus of Ada is not on safe arithmetic only, it's on functional safety at large: the code does what it is specified to do and nothing else. Ada shines in its specification power, how developers can express what the code is supposed to do (strong typing, ranges, contracts, invariants, generics, etc.). And then you can either check your code at "compile time" with SPARK [1], that provides a mathematical proof that you code follows the specification. SPARK also proves that you don't have buffer overflows or division by zero for instance. Or you can have checks inserted in the run-time code which greatly improves the benefits of testing as every deviation from specifications will be detected, not only the ones you decided to check in your tests. In terms of memory safety, Ada always had an edge on C/C++ because of the lower usage of pointers (see parameter modes [2]) and the emphasis on stack allocation. Now with the introduction of ownership in SPARK it's getting on par with Rust on that topic. [1] https://learn.adacore.com/courses/intro-to-spark/chapters/05_Proof_Of_Functional_Correctness.html#advanced-contracts https://learn.adacore.com/courses/intro-to-spark/chapters/05... [2] https://learn.adacore.com/courses/intro-to-ada/chapters/subprograms.html#parameter-modes https://learn.adacore.com/courses/intro-to-ada/chapters/subp...
- quotemstr 5y ago
  Interesting. I wasn't aware that safety in Ada had developed to this point. Maybe I'll have to take another look at the language!

m463 5y ago

I remember writing Ada (long ago) and my take was: it's nice to work on existing Ada code, but I thought it was tedious to write new code. there was also a lot of unchecked conversion under the hood. (disclaimer: I haven't really paid attention to newer versions of Ada)