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.)

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-perspec...

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.

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.

> 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.

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]

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 :-)

I was looking for something specific to type systems, but this is a good start.