Well sure if you lie to your specs all bets are off. Buffer overflows, bounds checking, use after free (if you're in a non-GCed language), resource leakage, etc. You're always at the mercy of your runtime system as soon as you lie about your pre-runtime checks, no matter what system you use, types or otherwise.

That's different than UB in the type system itself, which if you lie to it at worst just becomes inconsistent, but although that sounds quite scary, it's not really a big deal if you're not using dependent types as a theorem prover and you know where the inconsistency stems from.

Now perhaps your contention is that dependently typed systems tend to have weaker runtime checking, which I still disagree with. You do have weaker runtime guarantees with Idris 1's native code generator and of Agda's code extractor, but this is not true of Idris 1 on JS or its other code generators, which inherit their hosts' runtime systems, or Idris 2's native code generator, which inherits Chez Scheme's runtime system.

RE computations and functions yeah I definitely overreached. I somehow completely forgot that Hoare Logic has the ability to have unrestricted first-order logic. I got too fixated on JML, where in retrospect the difficulties only come from the awkward way that Java tries to handle higher-order methods like reduce (that was my initial impetus, verification of parallel reduce). I totally forgot I've done the isAssociative property in Dafny before and there it's exactly as you say, it's a function that you then put on top of a method (Dafny's notion of "computations").

The Lamport quote is a good reminder not to poo-poo different formalisms, but I've had a great time with systems like Dafny. I don't think dependent types are the holy grail of verification. My contention in fact is that the gulf between dependent types and contracts is not as large you're making it out to be.

Dependent types break down if you have pervasive mutability, i.e. as in an imperative language, for which Hoare Logic is very well-suited for. You have to express the mutability at a type level that's also is transparent enough to the type system to make assertions which makes things very annoying. (And no I don't use mutability/imperative as dirty words, most of my day-to-day work is in imperative languages and that's just fine by me, a lot of algorithms flow more naturally as imperative ones).

But if you have a language where everything is immutable, dependent types are fantastically expressive. And as long as you don't use the type inhabitants at runtime, their "proofs" or lack thereof are also very flexible. Hell, you could even generate a runtime assertion from a dependent type if you wanted to and have the compiler automatically insert those in place! You could even do that generation in a user-defined library without compiler support if dependently typed languages supported typecasing and didn't impose parametric polymorphism in all cases (useful in a non-dependently typed language, less useful in a dependently typed one). They don't, but that's a different story (for all my excitement about dependently typed languages, there's so many other ergonomic hurdles to get over first, as is true of a lot of the current state of code-based verification tools).

Indeed, dependent types and contracts converge in many ways if you have pervasive immutability. The main difference is that dependent types are more integrated into the language and don't have as many contract-isms. An invariant required by a function becomes just another argument. A lemma is just another function. Those contract-isms are necessary in a mutable environment (it would be rather painful to try to drum up some sort of type-indexed loop monad to try to express the notion of a loop-invariant in a dependently typed language, especially if the loop accesses non-local resources), but are not so much in an immutable one.

Oh BTW, speaking of limitations of formalisms, I'm pretty sure you're right on Twitter that Hillel Wayne's hyper-property isn't actually truly a hyper-property and can be described with the temporal quantifiers TLA+ has. A better example (that I don't think can be expressed in TLA+) is something like "variable independence," the statement that for any behavior where a variable "a" takes on some trace, there is another behavior such that "a" has a different trace, but all other parts of the behavior are the same. That is you can delete "a" from your spec and nothing would look different, no behavior would ever change (this requires either quantifying over all predicates or manipulating behaviors directly). Another example would be something like "x 'usually' takes n steps" for some definition of usually (mode, median, average, anything that's not a strict upper bound). Even expressing "n steps" in TLA+ is kind of wonky, but do-able with an additional counter variable (although that makes TLC unable to check termination).

Oh and of course since you've linked your own TLA+ link, many many thanks for your TLA+ series. It was an invaluable source right alongside Lamport's own materials when I was learning TLA+ on my own.