[pron]

> but the question can be broken down into many other sub-questions which can be answered formally, with a smaller core of sub-questions that are necessarily empirical.

I don't think this path is particularly fruitful, though. For one, the question of cost is still empirical. For another, researchers who study technique X are interested in answering the question of what it can do, but developers are interested in an entirely different question: of the many techniques of achieving their particular correctness requirements, which is the cheapest? This question is clearly empirical.

After all, engineers ultimately care about one thing only: the probability of system failure and its severity vs the cost of achieving this correctness goal. Since none of these factors is ever zero, I don't think the right path is to separate the layers and pick which ones we want to dial to 100%, especially when considering that at each layer, the difference between 99.99% and 100% can be 10x in cost. I think that a more holistic view is suitable in the vast majority of cases, which means that we may prefer less than 100% certainty at all layers. In particular, dialing some layers to 100% is almost certainly not the cheapest way to achieve some realistic correctness goal. Put differently, the mere fact that you could achieve your correctness goal by dialing the correctness of some of the layers to 100%, doesn't mean that's how you should achieve it and that there aren't cheaper ways.

[ithkuil]

I wonder if there is a framework where we can systematically reason about all those trade-offs we usually navigate empirically