formal logic gives us two properties to describe any evaluation procedure:
soundness – a sound jury will never send a guilty person free
completeness – a complete jury will never send an innocent person to jail
soundness and completeness are orthogonal: you can have any combination of soundness and completeness
a sound type system (or analysis) is one that rejects all erroneous programs, and a complete system accepts all correct programs
which is more important for static analysis?
many of the properties you really want to have verified (such as “does this rendering look right?”) don’t fall in the scope of the verification system
which is more important for type systems?
a sound type system is one that is not lenient – it rejects all invalid programs plus some number of valid programs
a complete type system accepts all valid programs, and some invalid ones to boot
the answer isn't quite as obvious as in static analysis
a programming language with a complete and unsound (static) type system has a fallback in the form of dynamic typing
Dependent type systems therefore blur the distinction between compile-time type checking and runtime type checking, and thus between static and dynamic typing.
Programmers dislike having the computer reject a program that would have run fine, simply because the computer couldn’t make sure it would run fine without actually running it
The target domain matters
For example, one hopes that the language for a program controlling an airliner’s fuel supply preferred soundness over completeness