5 ms·

> language with a garbage collector That is reasonable. Rust is not the only safe option. Re everything else....Rust should be seen as the beginning not the e

> language with a garbage collector That is reasonable. Rust is not the only safe option. Re everything else....Rust should be seen as the beginning not the end. All those model checking and other "post-hoc" analyses come with major productivity pitfalls. (Wrestling with some solver that may or may not be happy for spooky reasons is profoundly disheartening compared to wrestling with something elegant and compositional like a type system. Just as there is the ML family of languages and then SML with CakeML, Rust should continue being a fast-moving target where the occasional mistake might happen, but there is academic work revolving around the language which should create a CompCert/CakeML with time. Some aviation/auto software regulation is a legit, but frankly a some of it doubles as regularity ossification the industry secretly like as it creates a mote around existing businesses that have "evolved" compliance from the get-go. In that case, unproductivity is a feature, not a bug. I would not hold it up as a realistic model for these sorts of projects to aspire to. Without drastic changes to the way we found unprofitable FOSS foundation infrastructure, whenever productivity and security are at odds, the former will win over the latter.

grumblenum 5y ago
Using a mode checker on existing software is unproductive, but rewriting existing, working software that you have to shoehorn into a shape rustc (which had a miscompilation bug until 1.52.1, has no specifications or alternative implementations, right?) will compile is productive? Rust’s type system is elegant, but Agda, OCaml F#, F* and Haskell, which are in a whole different league of sophistication, are not? Furthermore, I’m not aware of any progress in “sealed rust” or “rust belt” other than raising grant money. I don’t think a certification is coming anytime soon. There are other verified compilers that could be used now, though. This argument sounds like rust for rust’s sake.
- Ericson2314 5y ago
  > Using a mode checker on existing software is unproductive, but rewriting existing, working software that you have to shoehorn into a shape rustc .... will compile is productive? The rewrite is a 1-time cost. > Rust’s type system is elegant, but Agda, OCaml F#, F* and Haskell, which are in a whole different league of sophistication, are not? I am primarily a Haskell user, and I already said I have nothing against GC. Those other languages (except for F#) are great! > has no specifications or alternative implementations That is a major downside (I work on GHC and wish it wasn't the only game in town) and affects all of those. That's why I put out SML and the CakeML implementation. SML lacks shiny new stuff but the grunt work has been done. I would certainly use SML over any variant of C for anything that needs dynamic allocation.
- steveklabnik 5y ago
  > which had a miscompilation bug until 1.52.1, All compilers have miscompilation bugs. Even ones that are proven correct. > has no specifications or alternative implementations, right? There is one alternative implementation that is good enough to bitwise reproduce rustc, there are a few other in-progress alternate implementations. > I’m not aware of any progress in “sealed rust” or “rust belt” That doesn't mean they haven't progressed. By the way, "Sealed Rust" is now called "Ferrocene" and is expected to GA in late 2022. https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/ferrocene/ > There are other verified compilers that could be used now, though. This is true, for sure. A compiler being verified is not a panacea.
  - grumblenum 5y ago
    A verified compiler is not panacea, but rust is because of unsubstantiated claims of its marketing professionals? This is total nonsense.
    - steveklabnik 5y ago
      Where did I say Rust is a panacea? A verified Rust compiler is a verified compiler, and wouldn’t be one either.
      - grumblenum 5y ago
        The stated goal of the grant program is to rewrite stable software many people use in Rust with the implied context being that C can’t be trusted, but Rust can be. I’m surprised that a language with no specified guarantees is favored over well established methods of verification. When you poopoo formal methods and verified compilers, it’s very hard to find a coherent logic behind RIIR, which offers much less in terms of security. Unless the exercise is a pretext to rationalize the grant money (which would be the real purpose).
        howinteresting 5y ago
        The formal verification researchers I've worked with love Rust, because its type system nails the basics so they can focus on proving more interesting properties. Rust and formal verification work really well together. You can formally verify properties in a small section of critical code, then use the type and lifetime systems to expand those properties to the whole codebase. It's not an either/or, it's a both/and.

grumblenum 5y ago

Using a mode checker on existing software is unproductive, but rewriting existing, working software that you have to shoehorn into a shape rustc (which had a miscompilation bug until 1.52.1, has no specifications or alternative implementations, right?) will compile is productive? Rust’s type system is elegant, but Agda, OCaml F#, F* and Haskell, which are in a whole different league of sophistication, are not? Furthermore, I’m not aware of any progress in “sealed rust” or “rust belt” other than raising grant money. I don’t think a certification is coming anytime soon. There are other verified compilers that could be used now, though. This argument sounds like rust for rust’s sake.

Ericson2314 5y ago
> Using a mode checker on existing software is unproductive, but rewriting existing, working software that you have to shoehorn into a shape rustc .... will compile is productive? The rewrite is a 1-time cost. > Rust’s type system is elegant, but Agda, OCaml F#, F* and Haskell, which are in a whole different league of sophistication, are not? I am primarily a Haskell user, and I already said I have nothing against GC. Those other languages (except for F#) are great! > has no specifications or alternative implementations That is a major downside (I work on GHC and wish it wasn't the only game in town) and affects all of those. That's why I put out SML and the CakeML implementation. SML lacks shiny new stuff but the grunt work has been done. I would certainly use SML over any variant of C for anything that needs dynamic allocation.
steveklabnik 5y ago
> which had a miscompilation bug until 1.52.1, All compilers have miscompilation bugs. Even ones that are proven correct. > has no specifications or alternative implementations, right? There is one alternative implementation that is good enough to bitwise reproduce rustc, there are a few other in-progress alternate implementations. > I’m not aware of any progress in “sealed rust” or “rust belt” That doesn't mean they haven't progressed. By the way, "Sealed Rust" is now called "Ferrocene" and is expected to GA in late 2022. https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/ferrocene/ > There are other verified compilers that could be used now, though. This is true, for sure. A compiler being verified is not a panacea.
- grumblenum 5y ago
  A verified compiler is not panacea, but rust is because of unsubstantiated claims of its marketing professionals? This is total nonsense.
  - steveklabnik 5y ago
    Where did I say Rust is a panacea? A verified Rust compiler is a verified compiler, and wouldn’t be one either.
    - grumblenum 5y ago
      The stated goal of the grant program is to rewrite stable software many people use in Rust with the implied context being that C can’t be trusted, but Rust can be. I’m surprised that a language with no specified guarantees is favored over well established methods of verification. When you poopoo formal methods and verified compilers, it’s very hard to find a coherent logic behind RIIR, which offers much less in terms of security. Unless the exercise is a pretext to rationalize the grant money (which would be the real purpose).
      - howinteresting 5y ago
        The formal verification researchers I've worked with love Rust, because its type system nails the basics so they can focus on proving more interesting properties. Rust and formal verification work really well together. You can formally verify properties in a small section of critical code, then use the type and lifetime systems to expand those properties to the whole codebase. It's not an either/or, it's a both/and.