> If you lie to the type system you just blow up at runtime, e.g. with an exception. Same as in any other language.
That depends on the runtime type system. If you can switch an int for a string (which is not hard in a dependent type system -- rely on the output of some silly arithmetic function that you only tested and omit a proof and use it in some
function that indexes types by integers, and you just might cast an int to a string), you will more likely get some UB and quite likely a security problem.
That's why I think that when it comes to correctness contracts are superior to types, and when it comes to tooling and organization, types are superior to contracts. Functional correctness is one area where flexibility is crucial, and soundness is never required because it's impossible anyway. Types, which are used for automatic transformation and code generation is one area where soundness is quite important; we shouldn't mix the two.
> Also out of curiosity, how do you express that, say, a static method with two arguments is associative in JML or any other contract system, Hoare Logic based or otherwise?
I don't know the arcana of JML, but I see no reason why, at least in principle, you couldn't do the same thing:
pure
\forall A x,y,z; foo(x, foo(y, z)) == foo(foo(x,y),z)
There's also no reason not to define a predicate `isAssociative`.
However, there is a difference -- not between specification with dependent types and contract systems, but between the semantics of the language where expressions mean something similar to "partial functions" (or even something similar to functions) and a language where they mean something else (like predicate transformers). In the latter, we don't in general represent computation as functions, so specifying something like associativity would normally be done as follows: define `isAssociative` on functions (not computations), and then specify that a computation computes a function (that is associative). That's how I would do it in TLA+, for example; I think that in Why3 as well.
Finally, it's important to remember that the very concepts can be different among languages. For example, all specifications of "higher-order" computations in functional languages (i.e higher order subroutines) become first order when you describe them in TLA+ (https://pron.github.io/posts/tlaplus_part3#higher-order-comp...). Lamport had this to say:
> Comparisons between radically different formalisms tend to cause a great deal of confusion. Proponents of formalism A often claim that formalism B is inadequate because concepts that are fundamental to specifications written with A cannot be expressed with B. Such arguments are misleading. The purpose of a formalism is not to express specifications written in another formalism, but to specify some aspects of some class of computer systems. Specifications of the same system written with two different formalisms are likely to be formally incomparable… Arguments that compare formalisms directly, without considering how those formalisms are used to specify actual systems, are useless.
The difference here is, then, not between specifying with types or with contracts, but between different formalisms.