6 ms·

Does a type system eliminate 100% of those errors? It eliminates those errors if you can be guaranteed that the underlying operating system calls and the hardw

Does a type system eliminate 100% of those errors? It eliminates those errors if you can be guaranteed that the underlying operating system calls and the hardware are always correct. That's pretty damn good but it's not 100%.

pron 7y ago
Right. Absolute guarantees can only apply to an algorithm, i.e. the abstract program, under certain assumptions about hardware and OS behavior. The correctness of software, a program running in the real world, is always probabilistic. There was an interesting case of a bug in the Java and Python sorting routines (TimSort) whose probability of manifestation in practice was about the same as a failure due to some hardware malfunction (bit-flip etc.). So you could think about it as if the algorithm was completely incorrect, but the program was about as correct as when running a totally correct algorithm.
- dnautics 7y ago
  I guess you could amend it to 'the type system prevents 100% of reasonably preventable errors of the class'!!
Twisol 7y ago
You’re absolutely correct that this depends on having the concrete semantics of the compiled program line up with the abstract semantics of the source language. What you may not notice is that the source language can indeed have a platform-independent abstract semantics, and it is that which 100% correctness is proved of. Once you leave the abstract semantics, you have the problem of proving your compiler to be a full and faithful transformer of program semantics. But this is a different problem space with different tools of analysis. It’s beneficial to start off already knowing that your source space is correct.
- pron 7y ago
  Sure, but there's also an assumption that the computer faithfully executes (w.r.t hardware spec) the machine instructions the compiler emits, and that is only true with probability. So system correctness is, therefore, always probabilistic. Whether, when and how it pays to absolutely guarantee certain aspects of it is a complex question (or, rather, a large set of questions) that can only be answered empirically.
  - Twisol 7y ago
    Oh, definitely. My point was only that verifying semantics at a layer, and verifying faithful translation between layers, are legitimately distinct activities that benefit from being considerd separately. I would consider "faithful execution of machine instructions" to be a translation between layers -- specifically, between the abstract semantics of the machine instructions and the concrete semantics of, well, physics! Siloing things this way helps us tighten down where faults can happen. It's true that faithful execution of a program can only be answered empirically -- 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.
    - pron 7y ago
      > 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.

pron 7y ago

Right. Absolute guarantees can only apply to an algorithm, i.e. the abstract program, under certain assumptions about hardware and OS behavior. The correctness of software, a program running in the real world, is always probabilistic. There was an interesting case of a bug in the Java and Python sorting routines (TimSort) whose probability of manifestation in practice was about the same as a failure due to some hardware malfunction (bit-flip etc.). So you could think about it as if the algorithm was completely incorrect, but the program was about as correct as when running a totally correct algorithm.

dnautics 7y ago
I guess you could amend it to 'the type system prevents 100% of reasonably preventable errors of the class'!!

Twisol 7y ago

You’re absolutely correct that this depends on having the concrete semantics of the compiled program line up with the abstract semantics of the source language. What you may not notice is that the source language can indeed have a platform-independent abstract semantics, and it is that which 100% correctness is proved of. Once you leave the abstract semantics, you have the problem of proving your compiler to be a full and faithful transformer of program semantics. But this is a different problem space with different tools of analysis. It’s beneficial to start off already knowing that your source space is correct.

pron 7y ago
Sure, but there's also an assumption that the computer faithfully executes (w.r.t hardware spec) the machine instructions the compiler emits, and that is only true with probability. So system correctness is, therefore, always probabilistic. Whether, when and how it pays to absolutely guarantee certain aspects of it is a complex question (or, rather, a large set of questions) that can only be answered empirically.
- Twisol 7y ago
  Oh, definitely. My point was only that verifying semantics at a layer, and verifying faithful translation between layers, are legitimately distinct activities that benefit from being considerd separately. I would consider "faithful execution of machine instructions" to be a translation between layers -- specifically, between the abstract semantics of the machine instructions and the concrete semantics of, well, physics! Siloing things this way helps us tighten down where faults can happen. It's true that faithful execution of a program can only be answered empirically -- 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.
  - pron 7y ago
    > 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.