4 ms·

The Linux kernel is fairly modular, I could definitely imagine rewriting subsystems by subsystems with fairly good ergonomics and safety. Like rewrite serial_co

by simias 6y ago

The Linux kernel is fairly modular, I could definitely imagine rewriting subsystems by subsystems with fairly good ergonomics and safety. Like rewrite serial_core.c in Rust and then let people write serial drivers in Rust. Then the SPI code. Then the I2C. Then USB etc... Easier said than done of course, and definitely a huge effort especially for such a huge project as the Linux kernel, but there's also a significant amount of resources that could be allocated to that task by several large institutions. I don't know if it's a good idea, or if ATS or something else could be better, but I think you're overly pessimistic. Also "the safety guarantees that Rust provides are neither unique nor complete", while technically true, is also borderline FUD-y. At least you should expand on what you have in mind here, because I doubt that there exists a programing language that deals with low level hardware configuration that could ever provide "complete guarantees" about anything. And beyond that, keep in mind that Rust provides a lot more than just safety guarantees, its syntax is lot more advanced that good old C in particular for anything dealing with types (including destructuring, matching, inference etc...). Even if you don't get "full" safety right away it can still be a much nicer language to code in (and I say that as somebody who knows C well and quite like it overall).

ghostwriter 6y ago
> Also "the safety guarantees that Rust provides are neither unique nor complete", while technically true, is also borderline FUD-y. At least you should expand on what you have in mind here, because I doubt that there exists a programing language that deals with low level hardware configuration that could ever provide "complete guarantees" about anything. I meant inability to implement within the boundaries of safe Rust certain data structures and algorithms that ATS can prove to be safe. To name a few: stack-allocated closures, and safe pointer arithmetic programming [1]. For instance, ring buffers in Rust use "unsafe" and at some point there was a logical CVE in vec_deque that broke one invariant of the unsafe block [2]. Safe implementation of the ring buffer in ATS could be found in [1] [1] http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf [2] https://gts3.org/2019/cve-2018-1000657.html https://gts3.org/2019/cve-2018-1000657.html
- gpm 6y ago
  > stack-allocated closures Rust routinely proves these to be safe. > safe pointer arithmetic programming You can't directly prove the pointer arithmetic safe with the compiler, but we routinely write a small amount of unsafe code which the programmer is confident in (and depending on the project that can mean an informal proof), and then re-use the data-structure that unsafe code created millions of times. A ring buffer is a great example. Vecdeque is implemented once in the standard library, everyone who uses Vecdeque can do so in completely safe code provided the small amount of code in Vecdeque is safe. This is orders of magnitude better than C, where every user of the ring buffer might make a mistake and cause a bug (or at least the API has no way of communicating that that is not the case, and in general the type system isn't expressive enough to make APIs that force that to be the case). It's not clear that taking the next step to proving the ring buffer implementation itself is correct to is actually worth the effort (it's not clear that it's not, but you need to make that cost benefit analysis, and I highly doubt it would be anywhere close to uncontroversially the case).
  - ghostwriter 6y ago
    > Vecdeque is implemented once in the standard library it is, what about other similar cases of using pointers in other data-structures and algorithms that are not part of the Rust standard library?
    - gpm 6y ago
      They are implemented once in a crate on crates.io and similarly re-used. Or in a code base like Linux with some unique requirements they'll be implemented once there and re-used many times there. As it turns out most code isn't datastructures with unique memory requirements (i.e. that can't be implemented in terms of other datastructures), most code just re-uses existing datastructures.
      - ghostwriter 6y ago
        > they are implemented once in a crate on crates.io and similarly re-used. this doesn't automatically prevent the code from containing CVE, does it? > As it turns out most code isn't datastructures with unique memory requirements most code that has been written in Rust so far. But when you enter a territory of OS kernels, unique memory requirements and data structures such as ring buffers and dynamic mutable trees are the things that have to be implemented according to the requirements, and we want them to be implemented as efficiently as C is capable of, and correctly. Falling back to "unsafe" is an option, but it's hardly an argument that supports the effort of bringing safety to such a kernel. But let's say that we've solved pointer issues. What about dependent types and totality checking? ATS has that [1] [2] [1] http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/INT2PROGINATS-BOOK-onechunk.html#programming-with-dependent-types http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/INT2PR... [2] http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/INT2PROGINATS-BOOK-onechunk.html#constructing_proofs_as_total_functions http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/INT2PR...

by simias 6y ago

ghostwriter 6y ago

> Also "the safety guarantees that Rust provides are neither unique nor complete", while technically true, is also borderline FUD-y. At least you should expand on what you have in mind here, because I doubt that there exists a programing language that deals with low level hardware configuration that could ever provide "complete guarantees" about anything. I meant inability to implement within the boundaries of safe Rust certain data structures and algorithms that ATS can prove to be safe. To name a few: stack-allocated closures, and safe pointer arithmetic programming [1]. For instance, ring buffers in Rust use "unsafe" and at some point there was a logical CVE in vec_deque that broke one invariant of the unsafe block [2]. Safe implementation of the ring buffer in ATS could be found in [1] [1] http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf [2] https://gts3.org/2019/cve-2018-1000657.html https://gts3.org/2019/cve-2018-1000657.html

gpm 6y ago
> stack-allocated closures Rust routinely proves these to be safe. > safe pointer arithmetic programming You can't directly prove the pointer arithmetic safe with the compiler, but we routinely write a small amount of unsafe code which the programmer is confident in (and depending on the project that can mean an informal proof), and then re-use the data-structure that unsafe code created millions of times. A ring buffer is a great example. Vecdeque is implemented once in the standard library, everyone who uses Vecdeque can do so in completely safe code provided the small amount of code in Vecdeque is safe. This is orders of magnitude better than C, where every user of the ring buffer might make a mistake and cause a bug (or at least the API has no way of communicating that that is not the case, and in general the type system isn't expressive enough to make APIs that force that to be the case). It's not clear that taking the next step to proving the ring buffer implementation itself is correct to is actually worth the effort (it's not clear that it's not, but you need to make that cost benefit analysis, and I highly doubt it would be anywhere close to uncontroversially the case).
- ghostwriter 6y ago
  > Vecdeque is implemented once in the standard library it is, what about other similar cases of using pointers in other data-structures and algorithms that are not part of the Rust standard library?
  - gpm 6y ago
    They are implemented once in a crate on crates.io and similarly re-used. Or in a code base like Linux with some unique requirements they'll be implemented once there and re-used many times there. As it turns out most code isn't datastructures with unique memory requirements (i.e. that can't be implemented in terms of other datastructures), most code just re-uses existing datastructures.
    - ghostwriter 6y ago
      > they are implemented once in a crate on crates.io and similarly re-used. this doesn't automatically prevent the code from containing CVE, does it? > As it turns out most code isn't datastructures with unique memory requirements most code that has been written in Rust so far. But when you enter a territory of OS kernels, unique memory requirements and data structures such as ring buffers and dynamic mutable trees are the things that have to be implemented according to the requirements, and we want them to be implemented as efficiently as C is capable of, and correctly. Falling back to "unsafe" is an option, but it's hardly an argument that supports the effort of bringing safety to such a kernel. But let's say that we've solved pointer issues. What about dependent types and totality checking? ATS has that [1] [2] [1] http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/INT2PROGINATS-BOOK-onechunk.html#programming-with-dependent-types http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/INT2PR... [2] http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/INT2PROGINATS-BOOK-onechunk.html#constructing_proofs_as_total_functions http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/INT2PR...