4 ms·

> 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 t

> 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...

gpm 6y ago
> this doesn't automatically prevent the code from containing CVE, does it? There are certainly tools to detect any known CVEs, and tools to help you audit the unsafe code that you are using. They don't provide rigorous proofs automatically of course, the same way the standard library is generally not rigorously proved to be correct. > But when you enter a territory of OS kernels, Nothing really changes, see redox as an example of a fairly "complete" kernel written in rust with a reasonably low amount of unsafe. > we want them to be implemented as efficiently as C is capable of, This is already the case with Rust's typical library system. Generic libraries in rust are not less efficient. In the real world rust datastructures are typically more efficient in my experience because the clean separation makes it easy to optimize the hell out of them. > What about dependent types That's a tool not a problem - you have yet to provide an argument that they are necessary and real world experience says that Rust achieves a meaningful amount of safety and convenience without them. > totality checking That's also a tool not a problem, and you could argue that rust's ADTs (enums) give you a weak version of it.
- ghostwriter 6y ago
  > There are certainly tools to detect any known CVEs, and tools to help you audit the unsafe code that you are using. so they don't automatically prevent the code from containing new CVEs. > That's a tool not a problem - you have yet to provide an argument that they are necessary and real world experience says that Rust achieves a meaningful amount of safety and convenience without them. I can argue along the same line that Rust is a tool not a problem, and that you need to prove that Rust has a "meaningful" amount of safety. When you say that something has "meaningful amount of sth" you should add to whom it is meaningful and based on what criteria. Or, alternatively, you can stay on a pure technical aspect of the matter and conclude that the safety part of the language is not complete. > That's also a tool not a problem, and you could argue that rust's ADTs (enums) give you a weak version of it. totality checking is not exhaustiveness checking, there are two more properties that enums are unable to express in any "weak" form - termination and productiveness.
c-cube 6y ago
ATS is also harder to understand[1] (in my experience) and has a fraction of a fraction of the adoption rust managed to get, despite being older. To me that suggests that rust is more approachable, has better documentation, and would be used by more people if supported by the kernel. [1] and really, I'm an OCaml developer and I can write rust; yet ATS' syntax looks terrible and very complicated. Its website and tooling make it appear like a research language made by one person. I don't know if that's really the case.

gpm 6y ago

> this doesn't automatically prevent the code from containing CVE, does it? There are certainly tools to detect any known CVEs, and tools to help you audit the unsafe code that you are using. They don't provide rigorous proofs automatically of course, the same way the standard library is generally not rigorously proved to be correct. > But when you enter a territory of OS kernels, Nothing really changes, see redox as an example of a fairly "complete" kernel written in rust with a reasonably low amount of unsafe. > we want them to be implemented as efficiently as C is capable of, This is already the case with Rust's typical library system. Generic libraries in rust are not less efficient. In the real world rust datastructures are typically more efficient in my experience because the clean separation makes it easy to optimize the hell out of them. > What about dependent types That's a tool not a problem - you have yet to provide an argument that they are necessary and real world experience says that Rust achieves a meaningful amount of safety and convenience without them. > totality checking That's also a tool not a problem, and you could argue that rust's ADTs (enums) give you a weak version of it.

ghostwriter 6y ago
> There are certainly tools to detect any known CVEs, and tools to help you audit the unsafe code that you are using. so they don't automatically prevent the code from containing new CVEs. > That's a tool not a problem - you have yet to provide an argument that they are necessary and real world experience says that Rust achieves a meaningful amount of safety and convenience without them. I can argue along the same line that Rust is a tool not a problem, and that you need to prove that Rust has a "meaningful" amount of safety. When you say that something has "meaningful amount of sth" you should add to whom it is meaningful and based on what criteria. Or, alternatively, you can stay on a pure technical aspect of the matter and conclude that the safety part of the language is not complete. > That's also a tool not a problem, and you could argue that rust's ADTs (enums) give you a weak version of it. totality checking is not exhaustiveness checking, there are two more properties that enums are unable to express in any "weak" form - termination and productiveness.

c-cube 6y ago

ATS is also harder to understand[1] (in my experience) and has a fraction of a fraction of the adoption rust managed to get, despite being older. To me that suggests that rust is more approachable, has better documentation, and would be used by more people if supported by the kernel. [1] and really, I'm an OCaml developer and I can write rust; yet ATS' syntax looks terrible and very complicated. Its website and tooling make it appear like a research language made by one person. I don't know if that's really the case.