4 ms·

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 aut

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.
    - 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
  My experience may be too specific to reason about productiveness with ATS when it comes to other developers. I knew some Haskell and I've already read the Idris book when I discovered ATS, and I knew some C from university courses. The proofs require the same mental model, totality check principles are the same, resource utilisation principles are the same, so for me the difference when comparing these two langauges is mostly about the things available apart from the common features: ATS prelude has many predefined constraint functions that facilitate low-level programming with pointers over unboxed data. I haven't tried F*, but from quick googling of "aliasing", it seems that a similar kind of checks can be achieved with view-changes in ATS (but please correct me if I'm missing the point) - http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3756.html http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/...
geofft 6y ago
> it can inline C without FFI I'm not sure what you mean by "FFI" (I would apply the term "FFI" to the way ATS interoperates with C, too), but you can certainly get cross-language LTO between C and Rust, since they both compile to LLVM IR. > 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 You can do this in Rust, too.
- ghostwriter 6y ago
  I meant not having to think about wrapping/boxing/unboxing, as they have exactly the same native data representation, so it's slightly different than LTO. But mine using "FFI" there was probably too vague and frivolous, I agree. > You can do this in Rust, too. not always within boundaries of safe Rust though (assuming each iteration is allowed to brings zero unsafe/unverified code), which undermines the initial safety argument.
  - geofft 6y ago
    > wrapping/boxing/unboxing, as they have exactly the same native data representation Rust's Box<T> and Option<Box<T>> have the same representation as a C pointer to the same type, so this is true of Rust too. You do have to wrap the type in source code to indicate what the ownership guarantees/contracts are. (Is this not also true of ATS? That is, if ATS code calls a C function that returns a pointer, how do you know how long that pointer is valid for and whether you're expected to free it?) But there is no runtime overhead/conversion. > which undermines the initial safety argument No, adding unsafe Rust does not undermine the safety argument (at least, no more than having any C somewhere in your address space does). See my reply in the comment section of TFA: https://lwn.net/Articles/830158/ https://lwn.net/Articles/830158/ (It's unfortunate that the Rust language used the "unsafe" keyword to mark blocks where you can access raw pointers, because it causes people to think that using such code is unsafe. Something like "manually_verified_safe" would have been better - the whole point of putting an "unsafe" block on a safe function is to write code that is safe to use that cannot benefit from the Rust compiler's checks. But at the boundary with C, it is impossible to have automated checks, because the relevant typing/safety information doesn't exist in C in the first place. It's no different from ATS code using $UN where you've manually verified that you're using a C function or C-created data in the way it's intended to be used.)

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.
  - 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
My experience may be too specific to reason about productiveness with ATS when it comes to other developers. I knew some Haskell and I've already read the Idris book when I discovered ATS, and I knew some C from university courses. The proofs require the same mental model, totality check principles are the same, resource utilisation principles are the same, so for me the difference when comparing these two langauges is mostly about the things available apart from the common features: ATS prelude has many predefined constraint functions that facilitate low-level programming with pointers over unboxed data. I haven't tried F*, but from quick googling of "aliasing", it seems that a similar kind of checks can be achieved with view-changes in ATS (but please correct me if I'm missing the point) - http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3756.html http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/...

geofft 6y ago

> it can inline C without FFI I'm not sure what you mean by "FFI" (I would apply the term "FFI" to the way ATS interoperates with C, too), but you can certainly get cross-language LTO between C and Rust, since they both compile to LLVM IR. > 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 You can do this in Rust, too.

ghostwriter 6y ago
I meant not having to think about wrapping/boxing/unboxing, as they have exactly the same native data representation, so it's slightly different than LTO. But mine using "FFI" there was probably too vague and frivolous, I agree. > You can do this in Rust, too. not always within boundaries of safe Rust though (assuming each iteration is allowed to brings zero unsafe/unverified code), which undermines the initial safety argument.
- geofft 6y ago
  > wrapping/boxing/unboxing, as they have exactly the same native data representation Rust's Box<T> and Option<Box<T>> have the same representation as a C pointer to the same type, so this is true of Rust too. You do have to wrap the type in source code to indicate what the ownership guarantees/contracts are. (Is this not also true of ATS? That is, if ATS code calls a C function that returns a pointer, how do you know how long that pointer is valid for and whether you're expected to free it?) But there is no runtime overhead/conversion. > which undermines the initial safety argument No, adding unsafe Rust does not undermine the safety argument (at least, no more than having any C somewhere in your address space does). See my reply in the comment section of TFA: https://lwn.net/Articles/830158/ https://lwn.net/Articles/830158/ (It's unfortunate that the Rust language used the "unsafe" keyword to mark blocks where you can access raw pointers, because it causes people to think that using such code is unsafe. Something like "manually_verified_safe" would have been better - the whole point of putting an "unsafe" block on a safe function is to write code that is safe to use that cannot benefit from the Rust compiler's checks. But at the boundary with C, it is impossible to have automated checks, because the relevant typing/safety information doesn't exist in C in the first place. It's no different from ATS code using $UN where you've manually verified that you're using a C function or C-created data in the way it's intended to be used.)