Totally 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 impossibl

Totally 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.