4 ms·

We have cosmical background events which cannot be shielded 100% and also cannot be predicted. This (among thousands of other reasons) means that you can never

We have cosmical background events which cannot be shielded 100% and also cannot be predicted. This (among thousands of other reasons) means that you can never prove 100% what any given program will do on a computer. Indeed, it's impossible to prove absolutely any fact about a real physical system. You prove things about abstract mathematical objects. Such a proof may be useful in practice when the assumptions you made for the proof are satisfied to a sufficient degree in a sufficient number of cases. Whether this is the case or not is ultimately a matter of judgement (and data, for which you have to use judgement in collecting/interpreting it, and data, for which...) By the way, the paper you're using to write proofs in mathematical logic is a physical system.

kccqzy 3y ago
You are missing the point. This article isn't talking about a real physical system, we are talking about abstract mathematical objects. The study of type system is to formalize the type system so they can be studied using logic alone. That's why there is the matter with soundness, the topic of this thread. Soundness is abstract, not physical. (The endless appeal to practicality and physicality is both tiring and irrelevant. Circles as a shape don't exist in the real world because you can't use physical objects to create a circle; at some point, perhaps at the level of atoms, the perfect smoothness of the ideal circle breaks down into discrete atoms. So circles don't exist. Does it bother me? No. Does it bother you? Evidently it does.)
- staunton 3y ago
  In practice, there is such a thing as "more or less sound" and there are no perfect circles. None of these things bother me. I responded to you because it seemed (no snark intended) that "more or less sound" things existing bothers you. The person who mentioned "more or less sound things" was referring to those things that exist in practice. The local discussion was (I thought) about type systems that exist in practice in the sense that a real practical C compiler has one. I think OP was justified in talking about this here, even if the article does not, because the theory exists at least in part to inform practice.

kccqzy 3y ago

You are missing the point. This article isn't talking about a real physical system, we are talking about abstract mathematical objects. The study of type system is to formalize the type system so they can be studied using logic alone. That's why there is the matter with soundness, the topic of this thread. Soundness is abstract, not physical. (The endless appeal to practicality and physicality is both tiring and irrelevant. Circles as a shape don't exist in the real world because you can't use physical objects to create a circle; at some point, perhaps at the level of atoms, the perfect smoothness of the ideal circle breaks down into discrete atoms. So circles don't exist. Does it bother me? No. Does it bother you? Evidently it does.)

staunton 3y ago
In practice, there is such a thing as "more or less sound" and there are no perfect circles. None of these things bother me. I responded to you because it seemed (no snark intended) that "more or less sound" things existing bothers you. The person who mentioned "more or less sound things" was referring to those things that exist in practice. The local discussion was (I thought) about type systems that exist in practice in the sense that a real practical C compiler has one. I think OP was justified in talking about this here, even if the article does not, because the theory exists at least in part to inform practice.