this post was submitted on 18 Sep 2024
286 points (97.4% liked)

Linux

48332 readers
937 users here now

From Wikipedia, the free encyclopedia

Linux is a family of open source Unix-like operating systems based on the Linux kernel, an operating system kernel first released on September 17, 1991 by Linus Torvalds. Linux is typically packaged in a Linux distribution (or distro for short).

Distributions include the Linux kernel and supporting system software and libraries, many of which are provided by the GNU Project. Many Linux distributions use the word "Linux" in their name, but the Free Software Foundation uses the name GNU/Linux to emphasize the importance of GNU software, causing some controversy.

Rules

Related Communities

Community icon by Alpár-Etele Méder, licensed under CC BY 3.0

founded 5 years ago
MODERATORS
 

Linus Torvalds Speaks on the the divide between Rust and C Linux developers an the future Linux. Will things like fragmentation among the open source community hurt the Linux Kernel? We'll listen to the Creator of Linux.

For the full key note, checkout: Keynote: Linus Torvalds in Conversation with Dirk Hohndel

The Register's summary: Torvalds weighs in on 'nasty' Rust vs C for Linux debate

(page 2) 43 comments
sorted by: hot top controversial new old
[–] [email protected] 3 points 2 months ago

I took notes for the benefit of anyone who doesn't like their info in video form. My attempt to summarize what Linus says:

He enjoys the arguments, it's nice that Rust has livened up the discussion. It shows that people care.

It's more contentious than it should be sometimes with religious overtones reminiscent of vi versus emacs. Some like it, some don't, and that's okay.

Too early to see if Rust in the kernel ultimately fails or succeeds, that will take time, but he's optimistic about it.

The kernel is not normal C. They use tools that enforce rules that are not part of the language, including memory safety infrastructure. This has been incrementally added over a long time, which is what allowed people to do it without the kind of outcry that the Rust efforts produce by trying to change things more quickly.

There aren't many languages that can deal with system issues, so unless you want to use assembler it's going to be C, C-like, or Rust. So probably there will be some systems other than Linux that do use Rust.

If you make your own he's looking forward to seeing it.

[–] [email protected] 1 points 2 months ago (1 children)

If you believe in ADTs, limiting mutation, & a type system that goes beyond Rust’s affine types + lack of refinements (including a interleaved proof system), you could be writing kernel code in ATS which compiles to C.

[–] [email protected] 2 points 2 months ago (2 children)
[–] [email protected] 1 points 2 months ago* (last edited 2 months ago) (1 children)

Correct me if I am wrong, but my understanding is that you use Coq to prove your theroem, then need to rewrite it in something else. I think there is some OCaml integration, but OCaml—while having create performance for a high level language & fairly predictable output—isn’t well-suited for very low-level kernel code. The difference in the ATS case (with the ML syntax similarity 🤘) is you can a) write it all in a single language & b) you can interweave proof, type, & value-level code thru the language instead of separating them; which means your functions need to make the proof-level asserts inside their bodies to satisfy the compiler if written with these requirements, or the type level asserting the linear type usage with value-level requirements to if allocating memory, must deallocate memory as well as compeletly prevent double free & use after free.

For those in the back: Rust can’t do this with its affine types only preventing using a resource multiple times (at most once), where linear types say you must use once & can only use once.

[–] [email protected] 2 points 2 months ago

You'r right that only OCaml and Haskell can be used as extraction target for Coq programs. However, it is possible to use Coq to write verified C software. On example is the Verified Software Toolchain that lets you translate C programs to a format that Coq understands and can prove theorems regarding their behavior.

[–] [email protected] 1 points 2 weeks ago

What exactly makes rust memory safe? That's the big selling point of it right? Is the compiler just more strict?

load more comments
view more: ‹ prev next ›