4 ms·

> Soundness means that every program that typechecks is valid. Completeness means that every valid program can be typed. I like this definition. Can someone li

> Soundness means that every program that typechecks is valid. Completeness means that every valid program can be typed. I like this definition. Can someone link to an authoritative article that elaborates on this statement?

eslaught 9y ago
This is a pretty standard definition (though sometimes the words get swapped). E.g. you see a very similar sentence in Wikipedia: > Informally, a soundness theorem for a deductive system expresses that all provable sentences are true. Completeness states that all true sentences are provable. https://en.wikipedia.org/wiki/Soundness#Relation_to_completeness https://en.wikipedia.org/wiki/Soundness#Relation_to_complete... You could probably follow the references there to more authoritative sources.
- jackfoxy 9y ago
  I was looking for something specific to type systems, but this is a good start.
- Izkata 9y ago
  Ehh, no. The definition on Wikipedia - at least the part you quoted, the rest is too jargony for me - is circular (and makes me think it's incorrect/missing something). The GP's sentence would require a third link, which missing means it isn't circular. Programs that can be typed will not necessarily be typecheck-able successfully. (I hope what I'm trying to get at makes sense and I'm not causing more confusion... what I have in mind is things like Java's ClassCastException - everything's typed, the typecheck passes, but it wasn't actually successful. Going by the Wikipedia quote, it would mean it wasn't actually possible for this exception to be thrown.)
  - a-saleh 9y ago
    I think this might be, because the definition seems to stem from mathematical notion of logic. And logicians usually want to have their logics sound, because if you can prove false statements, what is the point of your logic, right? So to distinguish between sound/unsound typesystem, I would look at it as if it were logic, where types are my theorems, and typechecking is attempt to find a proof. Of course, type-system for a language has to have some compromises, Java explicitly tells you, that even typechcecked program still will have runtime exceptions (like ClassCastException). In haskell you can still fall into an infinite loop, even though all the types flow through the system as expected :-)
  - systoll 9y ago
    The two statements are equivalent, and not circular. The type-checker 'proves' a statement of the form 'this program will never give values of one type to a statement expecting an incompatible type'. The fact that a Java program can pass typechecking, and then throw a type error at run time, is proof that Java's type system is unsound. https://dev.to/rosstate/java-is-unsound-the-industry-perspective https://dev.to/rosstate/java-is-unsound-the-industry-perspec...
    - Izkata 9y ago
      In the Wikipedia definition, the first phrase uses "all provable sentences" and "are true"; the second phrase uses "all true sentences" and "are provable". "true" and "provable" are equivalent in the two phrase here. In the other one, the first phrase uses "program that typechecks" and "is valid"; the second phrase uses "valid program" and "can be typed". "is valid" and "valid program" are equivalent, but "program that typechecks" and "can be typed" are not. So the two completeness/soundness definitions taken as a whole are not equivalent. That's what I was trying to get at with my example - it's not that the exception throws, but that the exception even exists.
      - eslaught 9y ago
        No, those are not equivalent at all. "Valid" means, intuitively, that if I skip the compile-time type checks, and run the program with the types checked at runtime. If the type system is sound, and the compile-time type checks all pass, then it is impossible to hit a runtime type error. More formally, a program is valid if the execution within the operational semantics (basically, the semantics of running the program) do not lead to an error. This is distinct from type checking correctly. Similarly, in formal logic "true" and "provable" are not equivalent. We'd like them to be, for sure, but the various incompleteness theorems ensure that we'll never be able to prove every possible true statement.
        Izkata 9y ago
        > Similarly, in formal logic "true" and "provable" are not equivalent. This tells me you've totally misunderstood my comment. More simply, "true" and "true" are equivalent, and "provable" and "provable" are equivalent. But while "valid" and "valid" are equivalent in the other definition, "typed" and "typechecked" are not.

eslaught 9y ago

This is a pretty standard definition (though sometimes the words get swapped). E.g. you see a very similar sentence in Wikipedia: > Informally, a soundness theorem for a deductive system expresses that all provable sentences are true. Completeness states that all true sentences are provable. https://en.wikipedia.org/wiki/Soundness#Relation_to_completeness https://en.wikipedia.org/wiki/Soundness#Relation_to_complete... You could probably follow the references there to more authoritative sources.

jackfoxy 9y ago
I was looking for something specific to type systems, but this is a good start.
Izkata 9y ago
Ehh, no. The definition on Wikipedia - at least the part you quoted, the rest is too jargony for me - is circular (and makes me think it's incorrect/missing something). The GP's sentence would require a third link, which missing means it isn't circular. Programs that can be typed will not necessarily be typecheck-able successfully. (I hope what I'm trying to get at makes sense and I'm not causing more confusion... what I have in mind is things like Java's ClassCastException - everything's typed, the typecheck passes, but it wasn't actually successful. Going by the Wikipedia quote, it would mean it wasn't actually possible for this exception to be thrown.)
- a-saleh 9y ago
  I think this might be, because the definition seems to stem from mathematical notion of logic. And logicians usually want to have their logics sound, because if you can prove false statements, what is the point of your logic, right? So to distinguish between sound/unsound typesystem, I would look at it as if it were logic, where types are my theorems, and typechecking is attempt to find a proof. Of course, type-system for a language has to have some compromises, Java explicitly tells you, that even typechcecked program still will have runtime exceptions (like ClassCastException). In haskell you can still fall into an infinite loop, even though all the types flow through the system as expected :-)
- systoll 9y ago
  The two statements are equivalent, and not circular. The type-checker 'proves' a statement of the form 'this program will never give values of one type to a statement expecting an incompatible type'. The fact that a Java program can pass typechecking, and then throw a type error at run time, is proof that Java's type system is unsound. https://dev.to/rosstate/java-is-unsound-the-industry-perspective https://dev.to/rosstate/java-is-unsound-the-industry-perspec...
  - Izkata 9y ago
    In the Wikipedia definition, the first phrase uses "all provable sentences" and "are true"; the second phrase uses "all true sentences" and "are provable". "true" and "provable" are equivalent in the two phrase here. In the other one, the first phrase uses "program that typechecks" and "is valid"; the second phrase uses "valid program" and "can be typed". "is valid" and "valid program" are equivalent, but "program that typechecks" and "can be typed" are not. So the two completeness/soundness definitions taken as a whole are not equivalent. That's what I was trying to get at with my example - it's not that the exception throws, but that the exception even exists.
    - eslaught 9y ago
      No, those are not equivalent at all. "Valid" means, intuitively, that if I skip the compile-time type checks, and run the program with the types checked at runtime. If the type system is sound, and the compile-time type checks all pass, then it is impossible to hit a runtime type error. More formally, a program is valid if the execution within the operational semantics (basically, the semantics of running the program) do not lead to an error. This is distinct from type checking correctly. Similarly, in formal logic "true" and "provable" are not equivalent. We'd like them to be, for sure, but the various incompleteness theorems ensure that we'll never be able to prove every possible true statement.
      - Izkata 9y ago
        > Similarly, in formal logic "true" and "provable" are not equivalent. This tells me you've totally misunderstood my comment. More simply, "true" and "true" are equivalent, and "provable" and "provable" are equivalent. But while "valid" and "valid" are equivalent in the other definition, "typed" and "typechecked" are not.