> static analysis (I'm not talking about deductively proving correctness)
What else could be the point to static analysis, if not completely ruling out bugs?
> vs. type systems.
Type-checking is a static analysis.
> We're talking about the relative merits of rewriting every line of C code out there in Rust vs. using verification tools,
Where exactly is the merit in deliberately choosing a more complicated approach to ruling out bugs?
> in order to increase our confidence in the safety of the code.
The conceptually simpler the approach, the more confidence one can have in the result.
> The argument isn't even about the quality of the result but the cost/benefit of the approach.
It's precisely in systems software where the cost of bugs is higher than everywhere else. Anything (types or otherwise) that simplifies the reasoning by which bugs can be ruled out in systems software is a strict improvement on the state of the art.
I don't think this is the place to debate verification theory and practice in general (I will be giving a talk about some aspects of the theory of software verification -- those that I've studied, at least -- at the upcoming Curry On conference in July, though not on the programming/spec language debate -- that is more religion than science; if you're interested, I would gladly debate various aspects of software correctness with you there; I think there’s a lot we disagree on). Here I'm talking about something else altogether.
What else could be the point to static analysis, if not completely ruling out bugs?
> vs. type systems.
Type-checking is a static analysis.
> We're talking about the relative merits of rewriting every line of C code out there in Rust vs. using verification tools,
Where exactly is the merit in deliberately choosing a more complicated approach to ruling out bugs?
> in order to increase our confidence in the safety of the code.
The conceptually simpler the approach, the more confidence one can have in the result.
> The argument isn't even about the quality of the result but the cost/benefit of the approach.
It's precisely in systems software where the cost of bugs is higher than everywhere else. Anything (types or otherwise) that simplifies the reasoning by which bugs can be ruled out in systems software is a strict improvement on the state of the art.