4 ms·

> First, lifting a new verification property into a type system requires changing the language or creating a new one, so it doesn't solve the problem (another r

> First, lifting a new verification property into a type system requires changing the language or creating a new one, so it doesn't solve the problem (another rewrite?). Much of the value in using type systems is that, precisely because they're limited, they force you to write programs whose proofs of correctness would be simpler than if you didn't follow a type discipline. This is true even if you use an external logic for reasoning about your program. In a language like Rust, I can often arrange things so that the burden of verification is split between type checking and simple high-school algebra calculations. What do I get in C? Gigantic yet intricate state spaces, which need to be split into subsets either manually or mechanically using who knows what heuristics. These subsets are in turn described by formulas containing lots of nested quantification, which is a lot more difficult for humans to deal with than just algebra. > Second, and more fundamentally, some properties cannot always be proven one way or another, but only admit sound classification as yes/no/maybe. Type systems don't usually work well with such properties. Type systems err on the side of safety: if no typing derivation can be constructed for your program, your program is wrong, even if your evaluation rules are untyped and your program wouldn't get stuck under them. > Even Rust would require a formal specification language for greater correctness This means nothing. Correctness is a binary question: your program is either right or wrong... > as the language itself cannot specify many interesting properties. ... regardless of whether you've mechanically verified it or not. > Whether, in terms of language design, it's better to unify the specification language and the programming language (as, say, Idris aims to do) or keep them separate is subject to a heated debate (dating all the way back to Dijkstra and Milner). It's ultimately a matter of ergonomics, and there's a big continuum in between “prove everything internally” and “prove everything externally”. Rust sits very comfortably at some point in the middle.

pron 10y ago
My response to Imm was about something a little different from my original point, which is this: Rust is absolutely amazing; I love it! It is leaps and bounds better than C! Yet none of that makes rewriting every line of C out there in Rust the most cost-effective way of improving software quality.
- catnaroek 10y ago
  > Yet none of that makes rewriting every line of C out there in Rust the most cost-effective way of improving software quality. What I know not to be cost-effective in the long run is working around C's inability to enforce its own abstractions. Anything that makes abstractions easier to protect is an improvement over what we have now.
  - pron 10y ago
    > working around C's inability to enforce its own abstractions But you don't need to. We are talking about rewriting internal code that no one intends to touch, not about improving APIs. > Anything that makes abstractions easier to protect is an improvement over what we have now. Sure, so wrap C code with Rust. That's a whole other matter than rewriting it.
    - catnaroek 10y ago
      > But you don't need to. We are talking about rewriting internal code that no one intends to touch, not about improving APIs. But it has to be touched, because it contains mistakes! > Sure, so wrap C code with Rust. That's a whole other matter than rewriting it. Reimplementing things in Rust from scratch has an important advantage: abstractions can be redesigned to maximize the extent to which the contract between API implementors and users is captured in types.
      - pron 10y ago
        > But it has to be touched, because it contains mistakes! Sure, but where exactly? Is manual translation into another language the best bang-for-the-buck approach you know for finding bugs? > Reimplementing things in Rust from scratch has an important advantage Of course it does! But is it the most cost-effective way to improve vast amounts of legacy code that isn't under active development? Just for the sake of argument, suppose some 10MLOC (which comprise a minuscule, nearly negligible, portion of all legacy C code) contain, say, 500 serious, dangerous bugs, 450 of them could be fixed in a Rust rewrite that would cost $10M, while, say, 400 of them could be fixed using C tools for the cost of, say $1M. Wouldn't it make much more sense not to do the rewrite for 10x the cost and 12% of added utility? Of course the situation could be much more in favor of Rust or in favor of C, but we don't know! Wouldn't it at least be far more responsible to use tools that would help us know where we stand for relatively little effort before we commit to one approach over the other?

pron 10y ago

My response to Imm was about something a little different from my original point, which is this: Rust is absolutely amazing; I love it! It is leaps and bounds better than C! Yet none of that makes rewriting every line of C out there in Rust the most cost-effective way of improving software quality.

catnaroek 10y ago
> Yet none of that makes rewriting every line of C out there in Rust the most cost-effective way of improving software quality. What I know not to be cost-effective in the long run is working around C's inability to enforce its own abstractions. Anything that makes abstractions easier to protect is an improvement over what we have now.
- pron 10y ago
  > working around C's inability to enforce its own abstractions But you don't need to. We are talking about rewriting internal code that no one intends to touch, not about improving APIs. > Anything that makes abstractions easier to protect is an improvement over what we have now. Sure, so wrap C code with Rust. That's a whole other matter than rewriting it.
  - catnaroek 10y ago
    > But you don't need to. We are talking about rewriting internal code that no one intends to touch, not about improving APIs. But it has to be touched, because it contains mistakes! > Sure, so wrap C code with Rust. That's a whole other matter than rewriting it. Reimplementing things in Rust from scratch has an important advantage: abstractions can be redesigned to maximize the extent to which the contract between API implementors and users is captured in types.
    - pron 10y ago
      > But it has to be touched, because it contains mistakes! Sure, but where exactly? Is manual translation into another language the best bang-for-the-buck approach you know for finding bugs? > Reimplementing things in Rust from scratch has an important advantage Of course it does! But is it the most cost-effective way to improve vast amounts of legacy code that isn't under active development? Just for the sake of argument, suppose some 10MLOC (which comprise a minuscule, nearly negligible, portion of all legacy C code) contain, say, 500 serious, dangerous bugs, 450 of them could be fixed in a Rust rewrite that would cost $10M, while, say, 400 of them could be fixed using C tools for the cost of, say $1M. Wouldn't it make much more sense not to do the rewrite for 10x the cost and 12% of added utility? Of course the situation could be much more in favor of Rust or in favor of C, but we don't know! Wouldn't it at least be far more responsible to use tools that would help us know where we stand for relatively little effort before we commit to one approach over the other?