2 ms·

> more or less sound There isn't more or less sound. There's really only sound or not.

by kccqzy 3y ago

AnimalMuppet 3y ago
Then there's really only "not". If you require perfect, 100% soundness in all circumstances, then nothing is sound. (Probably. We have things that we thought were sound, and later proved were not, so if you start with the list of things now that have no known holes, that's the upper limit of things that are possibly sound, modulo future holes.) If you seriously try for perfection, you can sometimes get pretty close. But if you insist on perfection or nothing, you usually get nothing.
- salawat 3y ago
  >If you require perfect, 100% soundness in all circumstances, then nothing is sound. Soundness in logic requires both valid form, and reasoning from true premises.
  - staunton 3y ago
    The problem is that in practice there is absolutely never any way to be 100% sure that the form is valid, the reasoning is correct, or that the premises are true. You can get pretty close to 100% but there might always be cases where you're not close enough "for all practical purposes".
staunton 3y ago
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.

> more or less sound There isn't more or less sound. There's really only sound or not.

by kccqzy 3y ago

> more or less sound There isn't more or less sound. There's really only sound or not.

Then there's really only "not". If you require perfect, 100% soundness in all circumstances, then nothing is sound. (Probably. We have things that we thought were sound, and later proved were not, so if you start with the list of things now that have no known holes, that's the upper limit of things that are possibly sound, modulo future holes.) If you seriously try for perfection, you can sometimes get pretty close. But if you insist on perfection or nothing, you usually get nothing.

salawat 3y ago
>If you require perfect, 100% soundness in all circumstances, then nothing is sound. Soundness in logic requires both valid form, and reasoning from true premises.
- staunton 3y ago
  The problem is that in practice there is absolutely never any way to be 100% sure that the form is valid, the reasoning is correct, or that the premises are true. You can get pretty close to 100% but there might always be cases where you're not close enough "for all practical purposes".

staunton 3y ago

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.