While this is true, it's critical to note that "valid" here doesn't mean "valid as in it follows the intention of the programmer who wrote it" but instead "valid as in it either terminates in a well-defined error condition or completes to an identically-typed result" (preservation and progress).

The engineering constraint is to ensure that the design and logic of the types themselves enable preservation-and-progress-validity to enforce meaningful semantic constraints. A sound and complete type system can still say things that aren't practically meaningful.

Note that most common type systems "crash" type-checked programs at runtime: null-pointer check failures, array-bound check failures, and (even, Java) co-variant array write check failures. So the line is fairly fuzzy.

Or just silently fail! Knowing the history of the Collections API and generics in Java, I know WHY this is like this, but Map.get taking an Object has resulted in way more bugs in previous code bases than I'd like to think about. If you have a Map<S, T> Java will silently take an object that has NOTHING to do with S and return null because that key is obviously not in the map. You can of course wrap that call behind functions that DO check the proper input type, but until you've been burnt by it you might not think to do that.

> If you have a Map<S, T> Java will silently take an object that has NOTHING to do with S and return null because that key is obviously not in the map

        Map map = new HashMap();
        map.put("one", 1);
        
        class Whatever {}

        Map<Whatever, Integer> whateverToIntMap = (Map<Whatever, Integer>) map;

        Integer i = whateverToIntMap.get("one");
        System.out.println("i = " + i);

Prints:

    i = 1

That's a consequence of generics type-erasure for backwards compatibility with non-generic code, so there _is_ a reason for `get` accepting any Object.

Like I said, I know the history and why it exists. I learned Java before 1.5 came out. That API existed long before generics did (I think 1.0 or earlier). If they had designed the language with generics in mind, they would have probably done it differently; hindsight is 20/20. Doesn't make it not a suboptimal API. I don't think there's a good way to fix it this late in the game without breaking old code, but such are the warts of backwards compatibility.

I'm curious, given Godels incompleteness theory, isn't it impossible to have both soundness and completeness in the same language?

Gödel's incompleteness is for proof systems for languages which contain enough arithmetic to express its own syntax. Lots of things don't go this far - first order predicate logic is sound and complete, for example (see Gödel's completeness theorem(!)).

Could you please expand on the soundness and completeness of first order logic? Isn't that false generally? Because you need a deductive/axiom system, so that you can ask the question of completeness/soundness. And ZFC is too strong, hence cannot prove its soundness and correctness at the same time. But you can formalize weaker systems in first order logic, that are provably complete and sound.

(It's been a year and a half since I took a course on this, so I apologize for any mistakes)

You do need to define a deductive/axiom system before you can ask the question. We can use a few different standard deductive systems. We require that the axioms are sound. Then the system is complete. (I think one should also always be able to prove false if the axioms aren't sound... but I don't recall proving that)

ZFC isn't too strong. That sounds like a contradiction, but it isn't, because we don't have a rich enough vocabularly in first order logic to state the problematic statements that make it either inconsistent or incomplete in stronger logic systems. Every true statement you can state about ZFC in first order logic is provable.

We can state a lot of things in first order logic about natural numbers or set theory which are not provable (in some given set of axioms like Peano axioms or ZFC, you can extend the axiom set but then one can generate a new unprovable statement if not a contradiction).

The issue here is first order logic is complete for statements that are true for all models of the axioms. As an example, imagine a infinite land which cant be completely described by any computable map(a programmable set of facts about the territory). The map will only tell you some true things about the territory.

But we can say this - if there is some statement that the map cant decide, then there are two different territories for both of which the map is accurate, and the statement is true for one territory and false for another. So the deductive system is complete description of true statements which hold for all territories for which the map applies.

But if we are interested in a single given territory, no computable system of facts suffices. For example deciding whether a diophantine equation has solutions in the standard set of Natural Numbers or a more familiar example for this site, whether a program halts. No computable deductive system(ie there is a program which generates all deductions) will suffice.

> It's been a year and a half since I took a course on this

Can you please recommend a MOOC/resource for learning more about this?

My only real exposure to it is the course I took, csc438 at UofT taught by Steven Cook.

There are pretty complete notes for the course as well as assignments here [0], but not videos or planned lessons. You certainly could learn about it by reading them, but I don't know if it would be the most efficient way.

[0] http://www.cs.toronto.edu/~sacook/csc438h/

Propositional calculus is sound and complete, first order predicate logic isn't.

fol logic is sound and complete (and effective). second order logic is not.

For reference: https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th...

Godel's theorem only applies to proof systems that can encode basic arithmetic, which most type systems cannot.

Would a type system that can verify whether array access is always in-bound implicitly encode arithmetic somehow? My gut feeling says yes, since I don't know how one would prove bounds without arithmetic, but I don't have the mathematical knowledge to back this up.

It would need a certain amount of arithmetic, but Presburger arithmetic (addition and constant multiplication, essentially) is complete and consistent and might be enough for all the array use we care about?

you can design a complete and sound type system in which any program can be checked in polynomial time.

https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...

Yes, although I would appeal to Rice's theorem rather than Gödel.

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

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

You could probably follow the references there to more authoritative sources.

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.