3 ms·

I think abstraction is key to efficiency. In order to have efficient systems we need to be able to prove properties of the software we write are correct with re

I think abstraction is key to efficiency. In order to have efficient systems we need to be able to prove properties of the software we write are correct with regards to our specifications. This is what abstractions do for us: they enable us to think in new semantic layers that are precise in the mathematical sense. This isn’t my idea, I just agree wholeheartedly with Conal Eliot. Resiliency is what we get when we want reliable systems but we cut corners with proving the correctness of the software we write: we add process supervisors, memory managers, tooling, exception handlers, etc: things that all cost us some efficiency in order to make our systems reliable enough to be useful. If we want efficiency, at scale, we need tools (languages really) that allow us to write proofs and generate code from these specifications.

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

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