5 ms·

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

> 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 conventional tooling reasons. It doesn't interoperate with C as well as other alternatives are capable of, whilst not being objectively better at safety guarantees either.

johncolanduoni 6y ago
How does ATS provide safety guarantees without additional semantic information about the C code it’s linking to? If it does require that, then you’re in the same boat as Rust: your choices are trivial interoperation with no safety at the interfaces or encoding the semantics of the C interface in the new language. The only difference I can think of is built in ability to inline C from headers (based on your comment about kmalloc), is that the case for ATS?
- ghostwriter 6y ago
  It's not only inclusion of the headers. ATS compiles to C, and it can inline C without FFI. The benefit that you receive is the ability to introduce gradual automated proofs around unchanged stable interfaces that are known to be safe. You start with inlining everything but the small core that is proven to be safe. Then you can iterate indefinitely at the desired pace to bring new layers of formally verified API in places of previously unverified C calls without breaking backward compatibility and expected runtime profiles (safe pointer-based memory access [1] and stack-allocated closures [2] as an example) [1] http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf [2] http://ats-lang.github.io/DOCUMENT/ATS2TUTORIAL/HTML/c1267.html http://ats-lang.github.io/DOCUMENT/ATS2TUTORIAL/HTML/c1267.h...
  - johncolanduoni 6y ago
    This may need fewer code changes (if the code in question is correct and the interfaces can possible be implemented in a safe way, that is) but it still requires developers to write proofs in a dependent type theory. I’ve only looked at ATS briefly, but I’m familiar with a lot of the other languages in the space (Idris, Fstar, etc.). Are ATS’s proof tactics drastically more productive/brief than those (F* in particular, which has great aliasing reasoning)? If not I think you’re radically overestimating the approachability of this route compared to Rust.
    - fluffy87 6y ago
      I’ve used ATS, Idris and Rust, and I find ATS way more cumbersome to use for writing proofs than idris. I’ve never used ATS to do what the GP is suggesting of incrementally wrapping C with proofs, but I can’t imagine this being simpler than just rewriting the C in Rust. You wouldn’t get the same proofs, but you would get memory and thread safety, which for many apps would be an incremental improvement. I haven’t taught ATS, but I found it harder to learn than Idris, and I can’t imagine C programmers which have a hard time with Rust learning it quicker than they would learn Idris or Rust.
      - ghostwriter 6y ago
        > but I can’t imagine this being simpler than just rewriting the C in Rust. sometimes it's impossible without falling back to unsafe Rust, which kind of undermines the initial incentive. C codebases heavily utilise pointer arithmetic programming. Simplicity is a good trait though, and there are a few promising initiatives in that regard in ATS3 - https://github.com/githwxi/ATS-Xanadu#project-description https://github.com/githwxi/ATS-Xanadu#project-description
        roca 6y ago
        "Sometimes" and "kind of" are doing a lot of work there. In reality most Rust code hardly ever needs to be unsafe and the existence of unsafe code in libraries you use hardly ever has any impact on the security and stability of what you ship, because there just isn't very much of it compared to the safe code. The "trophy cases" for Rust fuzzing bear witness to this. > C codebases heavily utilise pointer arithmetic programming. You don't write unsafe Rust code everywhere C code would use pointer arithmetic. You use safe Rust idioms and APIs instead. If it turns out that writing Linux drivers in Rust requires writing a lot of unsafe Rust code in each driver, then that would certainly be a failure. I don't see any reason to believe that will be the case.
deleted 6y ago
[deleted]

johncolanduoni 6y ago

How does ATS provide safety guarantees without additional semantic information about the C code it’s linking to? If it does require that, then you’re in the same boat as Rust: your choices are trivial interoperation with no safety at the interfaces or encoding the semantics of the C interface in the new language. The only difference I can think of is built in ability to inline C from headers (based on your comment about kmalloc), is that the case for ATS?

ghostwriter 6y ago
It's not only inclusion of the headers. ATS compiles to C, and it can inline C without FFI. The benefit that you receive is the ability to introduce gradual automated proofs around unchanged stable interfaces that are known to be safe. You start with inlining everything but the small core that is proven to be safe. Then you can iterate indefinitely at the desired pace to bring new layers of formally verified API in places of previously unverified C calls without breaking backward compatibility and expected runtime profiles (safe pointer-based memory access [1] and stack-allocated closures [2] as an example) [1] http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf [2] http://ats-lang.github.io/DOCUMENT/ATS2TUTORIAL/HTML/c1267.html http://ats-lang.github.io/DOCUMENT/ATS2TUTORIAL/HTML/c1267.h...
- johncolanduoni 6y ago
  This may need fewer code changes (if the code in question is correct and the interfaces can possible be implemented in a safe way, that is) but it still requires developers to write proofs in a dependent type theory. I’ve only looked at ATS briefly, but I’m familiar with a lot of the other languages in the space (Idris, Fstar, etc.). Are ATS’s proof tactics drastically more productive/brief than those (F* in particular, which has great aliasing reasoning)? If not I think you’re radically overestimating the approachability of this route compared to Rust.
  - fluffy87 6y ago
    I’ve used ATS, Idris and Rust, and I find ATS way more cumbersome to use for writing proofs than idris. I’ve never used ATS to do what the GP is suggesting of incrementally wrapping C with proofs, but I can’t imagine this being simpler than just rewriting the C in Rust. You wouldn’t get the same proofs, but you would get memory and thread safety, which for many apps would be an incremental improvement. I haven’t taught ATS, but I found it harder to learn than Idris, and I can’t imagine C programmers which have a hard time with Rust learning it quicker than they would learn Idris or Rust.
    - ghostwriter 6y ago
      > but I can’t imagine this being simpler than just rewriting the C in Rust. sometimes it's impossible without falling back to unsafe Rust, which kind of undermines the initial incentive. C codebases heavily utilise pointer arithmetic programming. Simplicity is a good trait though, and there are a few promising initiatives in that regard in ATS3 - https://github.com/githwxi/ATS-Xanadu#project-description https://github.com/githwxi/ATS-Xanadu#project-description
      - roca 6y ago
        "Sometimes" and "kind of" are doing a lot of work there. In reality most Rust code hardly ever needs to be unsafe and the existence of unsafe code in libraries you use hardly ever has any impact on the security and stability of what you ship, because there just isn't very much of it compared to the safe code. The "trophy cases" for Rust fuzzing bear witness to this. > C codebases heavily utilise pointer arithmetic programming. You don't write unsafe Rust code everywhere C code would use pointer arithmetic. You use safe Rust idioms and APIs instead. If it turns out that writing Linux drivers in Rust requires writing a lot of unsafe Rust code in each driver, then that would certainly be a failure. I don't see any reason to believe that will be the case.

deleted 6y ago

[deleted]