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

Supporting Linux kernel development in Rust

lwn.net

Post reply on HN
Print view View original

71–80 of 365 posts

Re: Supporting Linux kernel development in Rust

#71

Post by [deleted] »

ekidd wrote: post #62
ghostwriter wrote: post #30

I won't get tired of repeating the same comment in every topic that suggests Rust to be a great replacement of C in existing projects , that it isn't. The safety guarantees that Rust provides are neither unique nor complete, and if we discuss the amount of effort necessary for bringing new interfaces like the one this article mentions ("one can define a kmalloc_for_rust() symbol containing an un-inlined version"), we…

Yes, I've seen this comment a number of times now. ATS is a very interesting language! But there are a wide range of options for formal verification of systems programs, including the techniques used for the formally verified seL4 kernel, ATS, recent Ada work, TLA+, etc. Some of these tools have been very successful for certain projects. But the more powerful proof systems involve tradeoffs. Frequently, you need to i…

[deleted]

Re: Supporting Linux kernel development in Rust

#72

Post by ghostwriter »

ekidd wrote: post #62
ghostwriter wrote: post #30

I won't get tired of repeating the same comment in every topic that suggests Rust to be a great replacement of C in existing projects , that it isn't. The safety guarantees that Rust provides are neither unique nor complete, and if we discuss the amount of effort necessary for bringing new interfaces like the one this article mentions ("one can define a kmalloc_for_rust() symbol containing an un-inlined version"), we…

Yes, I've seen this comment a number of times now. ATS is a very interesting language! But there are a wide range of options for formal verification of systems programs, including the techniques used for the formally verified seL4 kernel, ATS, recent Ada work, TLA+, etc. Some of these tools have been very successful for certain projects. But the more powerful proof systems involve tradeoffs. Frequently, you need to i…

I agree with your comment, and I think we are mentioning the same question here, that is essential for the kind of discussion that this article raises - whether or not a suggested amount of effort to bring Rust into existing and well-established C codebase is a great idea and is justified on a technical merit basis, compared to the effort of brining more sophisticated formal proof assistants that aim at non-intrusive interfacing with C while being productive for the cause of promoting safe and formally-verified programming.

Python's gradual typing with MyPy demonstrated a great utility of static type checking that could be brought to existing project through many small and non-desruptive iterations. From my observation an learning of ATS, I expect even greater utility of gradual formal proofs that ATS enables for C. There are tons of successful C codebases, they are used in production around the world and contain a great amount of battle-tested knowledge. They just miss formal proofs that now could be gradually written for them.

Re: Supporting Linux kernel development in Rust

#73

Post by Athas »

gameswithgo wrote: post #65
ghostwriter wrote: post #30

I won't get tired of repeating the same comment in every topic that suggests Rust to be a great replacement of C in existing projects , that it isn't. The safety guarantees that Rust provides are neither unique nor complete, and if we discuss the amount of effort necessary for bringing new interfaces like the one this article mentions ("one can define a kmalloc_for_rust() symbol containing an un-inlined version"), we…

>The safety guarantees that Rust provides are neither unique nor complete, Well no language can ever have "complete" safety guarantees. But I would like to know what other languages offer the same set of guarantees without GC overhead. This would include: * the usual memory safety * no nulls * no undefined behavior * no data races Does ATS guarantee those things?

Yes, ATS can guarantee all those things and more. In particular, ATS allows you to write "unsafe" code, which you then prove safe with a mechanically verified proof. This is in contrast to unsafe Rust, which depends on programmer discipline, and has no (intra-language) mechanism for verification beyond the basic type system. You could say that Rust is all-or-nothing, while ATS allows gradual verification, as well as proving safe much more complex code than you can in Rust. I'm not going to claim that ATS is overall better than Rust - it's not - but it's a far more powerful language than Rust for safe systems programming. It's just that most people are not willing or able to pay the very high price in ergonomics. I recommend watching this presentation for a good idea of what ATS programming is like: https://www.youtube.com/watch?v=zt0OQb1DBko In short, it's about as user-friendly as an overheating nuclear reactor.

Re: Supporting Linux kernel development in Rust

#74

Post by scythe »

ghostwriter wrote: post #30

I won't get tired of repeating the same comment in every topic that suggests Rust to be a great replacement of C in existing projects , that it isn't. The safety guarantees that Rust provides are neither unique nor complete, and if we discuss the amount of effort necessary for bringing new interfaces like the one this article mentions ("one can define a kmalloc_for_rust() symbol containing an un-inlined version"), we…

> I won't get tired of repeating the same comment in every topic that suggests Rust [...] we should compare it to other existing solutions, like ATS [1]

One of the problems with repeating comments is that the previous replies are not incorporated into the discussion; for example, mine:

>Back when it was on the PL shootout, ATS was consistently in the top five for performance. However, it was also consistently the worst in program size

I looked into learning ATS some years ago before Rust existed, and shied away due to the complexity. It's been around much longer than Rust, and I think there's a reason it hasn't caught on: it's just too onerous. ATS might be appropriate for formally verified systems, but language ergonomics does matter, especially for a project with as many contributors as the Linux kernel.

Re: Supporting Linux kernel development in Rust

#75

Post by [deleted] »

ghostwriter wrote: post #49
gpm wrote: post #43

Earlier quoted context omitted.

Your evidence (that there are potentially other alternatives) doesn't support your claim (that Rust isn't a great C replacement). There can be multiple great C replacements. Not being "perfect" in terms of the guarantees you provide doesn't mean you aren't a great improvement. Nor would not providing any guarantees at all mean that a language is necessarily not a great improvement. That said, I would be very interest…

> Your evidence (that there are potentially other alternatives) doesn't support your claim (that Rust isn't a great C replacement). I didn't claim that Rust isn't a great replacement overall, I was specifically mentioning that it's not great for existing C codebases, by the fact that it requires significant work to replace internal interfaces that may be important for performance-, backward-compatibility- and convent…

[deleted]

Re: Supporting Linux kernel development in Rust

#76

Post by dbaupp »

rumanator wrote: post #63
stmw wrote: post #48

Earlier quoted context omitted.

ATS certainly looks interestinb, but it's an academic language (of which there are many) that most people probably haven't heard of... At some point, the momentum of a new programming language is just as important -- in practical terms -- as its formal attributes and qualities.

Your centering your criticism of ATS on popularity. Does an investment on PR trumps technical merit?

Popularity and momentum translate into (and are proxies for) important things like: library availability, long-term maintenance and support, more edge cases are explored (so less “research”, breaking new ground and bugs when going off the beaten track), tooling and even availability of teaching material like documentation and tutorials.

Re: Supporting Linux kernel development in Rust

#77

Post by chinigo »

rumanator wrote: post #63
stmw wrote: post #48

Earlier quoted context omitted.

ATS certainly looks interestinb, but it's an academic language (of which there are many) that most people probably haven't heard of... At some point, the momentum of a new programming language is just as important -- in practical terms -- as its formal attributes and qualities.

Your centering your criticism of ATS on popularity. Does an investment on PR trumps technical merit?

Popularity != PR.

Choosing an obscure language with little community support imposes real-world development costs: it's harder to find or ramp up new developers, there are fewer eyes identifying bugs in the implementation, tooling support can be subpar, documentation and blog posts are harder to find, etc.

(btw I know nothing about ATS so I'm not saying this is a good description of that language in particular.)

Re: Supporting Linux kernel development in Rust

#78

Post by outworlder »

ghostwriter wrote: post #30

I won't get tired of repeating the same comment in every topic that suggests Rust to be a great replacement of C in existing projects , that it isn't. The safety guarantees that Rust provides are neither unique nor complete, and if we discuss the amount of effort necessary for bringing new interfaces like the one this article mentions ("one can define a kmalloc_for_rust() symbol containing an un-inlined version"), we…

> The safety guarantees that Rust provides are neither unique nor complete

That sounds like "LEDs shouldn't be used for traffic lights because they don't melt snow", while ignoring all the benefits. Just add a heater where it is required.

Rust does add benefits. Are these worth the extra effort? It seems that some people think it's worth it.

Re: Supporting Linux kernel development in Rust

#79

Post by [deleted] »

gameswithgo wrote: post #65
ghostwriter wrote: post #30

I won't get tired of repeating the same comment in every topic that suggests Rust to be a great replacement of C in existing projects , that it isn't. The safety guarantees that Rust provides are neither unique nor complete, and if we discuss the amount of effort necessary for bringing new interfaces like the one this article mentions ("one can define a kmalloc_for_rust() symbol containing an un-inlined version"), we…

>The safety guarantees that Rust provides are neither unique nor complete, Well no language can ever have "complete" safety guarantees. But I would like to know what other languages offer the same set of guarantees without GC overhead. This would include: * the usual memory safety * no nulls * no undefined behavior * no data races Does ATS guarantee those things?

[deleted]
Post reply on HN