3 ms·
100% This is ideal. The trick for me though is that the foundational assumption on which to build our "proofs" change often and quickly. This creates drag on a
by blindhippo 3y ago
100% This is ideal.
The trick for me though is that the foundational assumption on which to build our "proofs" change often and quickly. This creates drag on any software project to keep up, and becomes untenable if the abstractions are wrong (i.e. the interfaces for components aren't adaptable). This is what I meant by designing with the assumption that one component could be replaced. To me it's a about the challenge of designing to reduce the need to "cut corners with proving ... correctness", if that makes sense.
- agentultra 3y agoTotally makes sense. It's an expensive enough process, still, that doing it at the scale that "non-verified" software is written at would be basically impossible. It makes sense that we've invested enough times in resiliency over the years that computer systems work as well as they do, let alone at all. We've squeezed a lot of efficiency out of our systems even without correctness. However I suspect we're beginning to reach a tipping point where it's becoming too expensive to avoid correctness and continue down this path of resiliency. At the scale of data-centers even small gains in efficiency have big effects. It's hard to get those kinds of gains without focusing on correctness. I'm hoping we'll find practical ways to compile dependently-typed programs and build theorem proving tools that scale to modern software practices and teams.