Dynamic type systems are not inherently more open

This seems like too strong of a statement. Every language that allows for nontotal functions has a type system allowing for unsound proofs. This does not mean the type system is compromised to the point of undefined behavior.

Dependent Haskell is explicitly going to be unsound even in the presence of totality (type in type). Idris allows for partial functions by default (although you do need to annotate if you want to use it at the type level and the compiler doesn't know it's total). Dependent type systems are not required to be sound by any means.

If you lie to the type system you just blow up at runtime, e.g. with an exception. Same as in any other language.

Leaving that aside, my point is that as long as you don't need your proofs at runtime, you don't have to use a deductive proof with dependent types! Substitute the property check thing there with a model checker if you want 100% assurance, but you don't even need a sound verification! If you're okay with just 99% confidence instead of 100% then just do the property test and be done with it (that's my example with concat and chrisdone is talking about when you would run the property test). If you're feeling really adventurous just assert the statement without proof and move on. If you don't run it at runtime how you prove something or even if you do is up to you.

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 suspect you can, but I also suspect it looks annoying and hacky where you essentially encode a function application counter in your ambient state and have to basically make an inductive statement. EDIT: ah ha in JML you have the keyword pure that extends Hoare Logic so I suppose you do an assert with pure? But then how do you express the general notion of associativity? By requiring purity as a precondition and then writing out the condition again? Can you specify purity as a precondition? I'm not sure how you do that, presumably you'd need JML to be able to recognize a SAM class and then be able to tie purity to that, which seems hard if not built-in.

Whereas with dependent types it looks very similar to the usual notation.

  (x, y, z : A) -> x `op` (y `op` z) = (x `op` y) `op` z

  op : A -> A -> A

  isAssociative : (op : a -> a -> a) -> ((x, y, z: a) -> x `op` (y `op` z) = (x `op` y) `op` z)

The requirement for dynamic typing can either come from the language, or it can be "Greenspunned", or some combination of the two.

For instance, in that data we can construct objects, and we can write expressions which interrogate an object's type.

Thus, that is an example of input data whose processing requires dynamic typing.

  std::vector> s;
  s.push_back({"a", 1});
  s.push_back({"b", 2});
  s.push_back({"c", 3});

I think you're making the same point that I am, but perhaps from the opposite direction.

Of course contracts are more general, but the aspects of a contract that you can prove automatically in advance are similar to what you can typically do with a good static type system, and the limits of a decent static type system fall around the point that contracts become more powerful but only at runtime. This isn't an accident, it's a fundamental equivalence.

For example, you mentioned SPARK before. One of the interesting things about SPARK is the extra flexibility you have when adding constraints on integer data types. The proof system can verify certain properties (or warn you that it can't). That can provide safeguards against, among other things, some very common logic errors like out-of-bounds access to data structures.

However, the fact that we're dealing with integer values is very helpful in this respect. Lots of behaviour is fully specified no matter how much we manipulate those values. For the same reason, dependent type systems can often provide similar guarantees. The curious property of C++ templates that they allow integer as well as type parameters has allowed for all kinds of handy metaprogramming tricks along similar lines.

Now, suppose we're working in the much less convenient world of floating point values. It's still helpful to have warnings about, for example, potential underflow or overflow conditions, for all the same reasons. However, given the inherent imprecision of floating point data, it is impossible to prove such conditions in advance in almost any non-trivial case. You can certainly have a precondition on a relevant function that, for example, adding two input values must not entirely lose the smaller value due to loss of significance, but you won't find out about inputs that violate the contract until you run your program.

Even when formal proofs are used, the specification is done in a contract system, not a dependent type system.

You can do the specification in any number of ways. Unless you want to classify all of mathematics as "a contract system", which is true in a sense but so general as to lose any useful meaning of the term, your statement above is too strong.