4 ms·

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 st

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.
- systoll 9y ago
  The distinction you're drawing is imprecision in the type-checking statement. > "program that typechecks" and "can be typed" are not [equivelent] Sure. The above statement be more rigorous if it said 'has consistent types assigned to it by the type checker' and 'will be assigned consistent types when run through the type checker'. [And, yes, every runtime ClassCastError demonstrates Java's type-checker's unsoundness, and a 'Sound Java' would have no need for the concept]

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.
systoll 9y ago
The distinction you're drawing is imprecision in the type-checking statement. > "program that typechecks" and "can be typed" are not [equivelent] Sure. The above statement be more rigorous if it said 'has consistent types assigned to it by the type checker' and 'will be assigned consistent types when run through the type checker'. [And, yes, every runtime ClassCastError demonstrates Java's type-checker's unsoundness, and a 'Sound Java' would have no need for the concept]