7 ms·

As one of the developers of this patchset, here is my simple answer: try it. I'd love to see it. I know Rust; I don't know Frama-C or Idris or Ada. What little

by geofft 5y ago

As one of the developers of this patchset, here is my simple answer: try it. I'd love to see it. I know Rust; I don't know Frama-C or Idris or Ada. What little I know of Ada indicates that it doesn't actually solve the problem because it doesn't have safe dynamic memory allocation. Ada advocates have told me I'm wrong and there's some new thing (inspired by Rust) that does this. Maybe! I'm not sure there's any benefit to the world in arguing it; someone skilled in Ada should just write something and show how it would actually work. Write a kernel module with any of those techniques, send in a patch, and see what people say. Any effective means of making the kernel less buggy is great. It doesn't have to be Rust. I claim that Rust is effective because, well, those patches are there, and frankly I haven't been doing any work for this project in almost a year and we're getting so many enthusiastic contributors. So, apparently, a lot of other people also know or are willing to learn Rust. Maybe it's actually better than the alternatives you mention; maybe it just has better documentation. I don't know. I'm not claiming Rust is perfect, just that it's empirically likely to solve the problem. If you can get together a community of folks who can do any of these other approaches, that would be fantastic. Try it!

pjmlp 5y ago
> What little I know of Ada indicates that it doesn't actually solve the problem because it doesn't have safe dynamic memory allocation. It does, just not the way most are used to it. Surely if one wants to code like malloc()/free(), free() is unsafe in Ada and requires the Ada version of unsafe {} However many type constructions in Ada do dynamic allocation by themselves, including on the stack. If memory allocation fails, an exception is thrown and a retry with less memory requirements is a possible execution path. Ada also has RAII since Ada95 (controlled types), and yes SPARK formal specification now allows for ownership rules.
- tialaramex 5y ago
  > If memory allocation fails, an exception is thrown and a retry with less memory requirements is a possible execution path. So, since we're talking about the Linux kernel, that's a red flag straight away. Notice a whole section of this new LKML post is about their implementation of Rust's alloc crate? Linus doesn't want useless exceptions here and has previously objected on that basis. Meanwhile... Over in the C++ world they have this same behaviour. For them these exception handlers are a fiction, in reality popular standard libraries (never mind everything else you're using) will blow up in low memory and it's game over. Maybe Ada does a lot better. Maybe.
  - pjmlp 5y ago
    Linux kernel doesn't have clearance for high integrity computing, or being in control of machines responsible for human life's, Ada does. Ada also has no exception allowed profiles and other mechanisms. HN is not the place to hold a lecture on Ada features. It is not a maybe, rather lack of knowledge.
    - short_sells_poo 5y ago
      You seem to be arguing as if this effort should have gone to Ada instead. So go ahead and do it. There's a group of people who are trying to get kernel support for Rust. This is not a statement about Rust being superior to Ada or Ada's (in)suitability for the same job. It's only a statement that this group of people likes rust for it's safety features. I'm sure they are all aware that there are other, even safer languages, but these people like Rust. We can lead academic discussions about which language is safer/better/leaner/whatever-er, but the fact is that Rust has a larger and growing mindshare so this effort is unsurprising. For Ada, the solution isn't to try and prove to anonymous forum goers it would've been better choice if only people recognized the fact. The solution is to mobilize the Ada community to put the same amount of effort into the publicity and marketing (yes, the bad M word) of their ecosystem. Ada clearly lives on in many safety critical systems, but judging by the admittedly biased topic frequency on HN and other technical sites, it has a tiny community who mostly keep to themselves. That's fine, but then don't be surprised when it's Hip Language X that gets the headlines and these sort of efforts.
      - pjmlp 5y ago
        That effort has been happening for production code in high integrity systems since Ada was released to the world in 1983. My only point is how many in the Rust community advocate as if Rust would be the first language having features, that actually were already in Ada for the past decades. As for Ada on Linux, naturally Linus would never go along it. A C kernel guy liking a language with Pascal syntax, a community that worships a paper that hasn't been true in the Pascal world since early 80's, not even at gunpoint. If you want to see a use case where Ada was chosen against Rust, check NVidia's project for self driving vehicles firmware.
grumblenum 5y ago
As one of the developers of this patchset, can you comment on how these contributions will be licensed? Can you also comment on how a third party can verify or audit the output of a compiler without a specification? >just that it's empirically likely to solve the problem. Can you comment on what empirical evidence you based this statement on?
- geofft 5y ago
  > As one of the developers of this patchset, can you comment on how these contributions will be licensed? Yes, I can comment on this. The licensing is the same as any other submission to the Linux kernel. See https://www.kernel.org/doc/html/latest/process/license-rules.html https://www.kernel.org/doc/html/latest/process/license-rules... for Linux kernel licensing in general and also https://www.kernel.org/doc/html/latest/process/submitting-patches.html#sign-your-work-the-developer-s-certificate-of-origin https://www.kernel.org/doc/html/latest/process/submitting-pa... for the meaning of the Signed-off-by lines. > Can you also comment on how a third party can verify or audit the output of a compiler without a specification? I imagine it's pretty similar to how you verify or audit the output of a compiler with a specification. If you can show me an example of the sort of verification or audit you envision, I can perhaps give you a more helpful comment. We do not make any claims about verified or audited compiler outputs or compliance with specifications, and to the best of my knowledge, the Linux kernel does not currently verify or audit any compiler outputs, so I'm not sure I follow why I would be particularly qualified to comment on it, but I could maybe point you at some interesting research. > Can you comment on what empirical evidence you based this statement on? Yes, I did comment on this, in the paragraph you quoted. If you'd like me to expand on something can you clarify?
  - grumblenum 5y ago
    >I imagine it's pretty similar to how you verify or audit the output of a compiler with a specification. I must be missing the humor here. You can test against a specification to verify implementation. Testing an implementation against itself is meaningless. I would think that this is obvious. Also I don't typically use the word "empirical" to indicate purely qualitative assessments or intuition. You also provided a dead link.

by geofft 5y ago

pjmlp 5y ago

> What little I know of Ada indicates that it doesn't actually solve the problem because it doesn't have safe dynamic memory allocation. It does, just not the way most are used to it. Surely if one wants to code like malloc()/free(), free() is unsafe in Ada and requires the Ada version of unsafe {} However many type constructions in Ada do dynamic allocation by themselves, including on the stack. If memory allocation fails, an exception is thrown and a retry with less memory requirements is a possible execution path. Ada also has RAII since Ada95 (controlled types), and yes SPARK formal specification now allows for ownership rules.

tialaramex 5y ago
> If memory allocation fails, an exception is thrown and a retry with less memory requirements is a possible execution path. So, since we're talking about the Linux kernel, that's a red flag straight away. Notice a whole section of this new LKML post is about their implementation of Rust's alloc crate? Linus doesn't want useless exceptions here and has previously objected on that basis. Meanwhile... Over in the C++ world they have this same behaviour. For them these exception handlers are a fiction, in reality popular standard libraries (never mind everything else you're using) will blow up in low memory and it's game over. Maybe Ada does a lot better. Maybe.
- pjmlp 5y ago
  Linux kernel doesn't have clearance for high integrity computing, or being in control of machines responsible for human life's, Ada does. Ada also has no exception allowed profiles and other mechanisms. HN is not the place to hold a lecture on Ada features. It is not a maybe, rather lack of knowledge.
  - short_sells_poo 5y ago
    You seem to be arguing as if this effort should have gone to Ada instead. So go ahead and do it. There's a group of people who are trying to get kernel support for Rust. This is not a statement about Rust being superior to Ada or Ada's (in)suitability for the same job. It's only a statement that this group of people likes rust for it's safety features. I'm sure they are all aware that there are other, even safer languages, but these people like Rust. We can lead academic discussions about which language is safer/better/leaner/whatever-er, but the fact is that Rust has a larger and growing mindshare so this effort is unsurprising. For Ada, the solution isn't to try and prove to anonymous forum goers it would've been better choice if only people recognized the fact. The solution is to mobilize the Ada community to put the same amount of effort into the publicity and marketing (yes, the bad M word) of their ecosystem. Ada clearly lives on in many safety critical systems, but judging by the admittedly biased topic frequency on HN and other technical sites, it has a tiny community who mostly keep to themselves. That's fine, but then don't be surprised when it's Hip Language X that gets the headlines and these sort of efforts.
    - pjmlp 5y ago
      That effort has been happening for production code in high integrity systems since Ada was released to the world in 1983. My only point is how many in the Rust community advocate as if Rust would be the first language having features, that actually were already in Ada for the past decades. As for Ada on Linux, naturally Linus would never go along it. A C kernel guy liking a language with Pascal syntax, a community that worships a paper that hasn't been true in the Pascal world since early 80's, not even at gunpoint. If you want to see a use case where Ada was chosen against Rust, check NVidia's project for self driving vehicles firmware.

grumblenum 5y ago

As one of the developers of this patchset, can you comment on how these contributions will be licensed? Can you also comment on how a third party can verify or audit the output of a compiler without a specification? >just that it's empirically likely to solve the problem. Can you comment on what empirical evidence you based this statement on?

geofft 5y ago
> As one of the developers of this patchset, can you comment on how these contributions will be licensed? Yes, I can comment on this. The licensing is the same as any other submission to the Linux kernel. See https://www.kernel.org/doc/html/latest/process/license-rules.html https://www.kernel.org/doc/html/latest/process/license-rules... for Linux kernel licensing in general and also https://www.kernel.org/doc/html/latest/process/submitting-patches.html#sign-your-work-the-developer-s-certificate-of-origin https://www.kernel.org/doc/html/latest/process/submitting-pa... for the meaning of the Signed-off-by lines. > Can you also comment on how a third party can verify or audit the output of a compiler without a specification? I imagine it's pretty similar to how you verify or audit the output of a compiler with a specification. If you can show me an example of the sort of verification or audit you envision, I can perhaps give you a more helpful comment. We do not make any claims about verified or audited compiler outputs or compliance with specifications, and to the best of my knowledge, the Linux kernel does not currently verify or audit any compiler outputs, so I'm not sure I follow why I would be particularly qualified to comment on it, but I could maybe point you at some interesting research. > Can you comment on what empirical evidence you based this statement on? Yes, I did comment on this, in the paragraph you quoted. If you'd like me to expand on something can you clarify?
- grumblenum 5y ago
  >I imagine it's pretty similar to how you verify or audit the output of a compiler with a specification. I must be missing the humor here. You can test against a specification to verify implementation. Testing an implementation against itself is meaningless. I would think that this is obvious. Also I don't typically use the word "empirical" to indicate purely qualitative assessments or intuition. You also provided a dead link.