> I think in order to appreciate DbC [...] one needs to have some idea of "Program Correctness" concepts in the lineage of Floyd/Hoare/Dijkstra and Meyer.

Agreed. To me, full-program (or system) formal verification is something I'd love to have, but I also acknowledge that even champions of formal methods (like Tony Hoare you mentioned) doubt its practicality, due to how large our software systems tend to be nowadays. If so, then let's take as much as we can from those methods (powerful, expressive type systems) and let's complement that with proper infrastructure for ensuring correctness (contracts, invariants, various kinds of automated tests) that are weaker, but much more applicable in practice.

Unfortunately, we're still stuck in a place where a plain `assert` - basically a "goto of ensuring correctness" - needs to be introduced to people with posts like the OP's...

> To me this is the need of the hour and yet i don't see people talking about it

Yes, I feel the same. I think the reason here is that we (programmers, collectively) didn't really take correctness of our programs seriously before, so there's just not much awareness about the research and work done in this problem space. Many people now are ready to admit that yes, we do need stronger, more comprehensive and better integrated tools for controlling, showing, and ensuring correctness - but the need for them arrived so quickly (and along with so many other, serious changes to the craft), that they simply haven't been able to catch up on the prior work fast enough. It'll probably take a few years, at least, for the urgent need for better tools to become widely recognized. It'll take even more time to get to usable implementations.

> (gradual typing is whole another beast altogether)

It's actually not. Contracts in Racket are duals of types (well, not fully, since you can put arbitrary code in a predicate and make that into a contract; however, that's more of an escape hatch than the default use of contracts in Racket). Typed Racket can wrap a typed value in a contract that guarantees that, when the value comes back, it exactly conforms to its type. This way, you can avoid expensive casts. Moreover, Typed Racket has refinement types (ie. that a given int will always be greater than 0), and these refinements have direct contract equivalents, too. So a Typed Racket value can be statically proven to have that property on the typed side, and then you don't have to check or prove it again when it comes back from the untyped world.

I believe this is an extremely neat capability that ties types and contracts together, opening some very interesting possibilities. Like, if a contract can be expressed as a refinement on a type, and we already have support for that in the type checker, we can automatically promote such contracts into types! That's huge, because if the contracted value never leaves a well-typed environment, we can eliminate all runtime checks without affecting correctness. It also addresses the most common problem with contracts (and assertions): runtime overhead.

I'm aware of all that because I decided to build an environment that would blend a fast, interactive development loop, an isolated environment in which agents can comfortably live, and an expansive toolkit for checking and ensuring correctness. I'm building it on top of Pharo Smalltalk, Glamorous Toolkit, and an extended Gradualtalk implementation that would also handle contracts. There are some problematic parts, but if I manage to achieve my goals in a Smalltalk image, I feel like it'll prove it can be achieved in literally every other environment, too :)

EDIT: Forgot to mention, there's a pretty extensive list of papers on contracts and gradual typing here: https://samth.github.io/gradual-typing-bib

EDIT: "Types to contracts" is already presented in papers I referenced before (Typed Racket ones); forgot to mention the "contracts to types" (or rather, static verification of contracts) part: "Soft Contract Verification for Higher-Order Stateful Programs" and "Soft Contract Verification" by Phuc C. Nguyen et al.