4 ms·

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

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.
- Ar-Curunir 6y ago
  The point of Rust is not to eliminate unsafe, but to minimize it and make the actual unsafe operations visible and easily auditable.
  - ghostwriter 6y ago
    ok, I'm fine with that, the question is why it is technically better for Linux Kernel than a proper formally-verified implementation that doesn't require Rust toolchain?
    - Ar-Curunir 6y ago
      Because I can bet that it’s easier to write correct Rust than to write correct ATS.

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.
Ar-Curunir 6y ago
The point of Rust is not to eliminate unsafe, but to minimize it and make the actual unsafe operations visible and easily auditable.
- ghostwriter 6y ago
  ok, I'm fine with that, the question is why it is technically better for Linux Kernel than a proper formally-verified implementation that doesn't require Rust toolchain?
  - Ar-Curunir 6y ago
    Because I can bet that it’s easier to write correct Rust than to write correct ATS.