[ratmice]

To me at least, the most difficult part of verifying rust code has been the lack of any pre/post conditions on the standard library, I quite often have ended up rewriting chunks of the std library, pulling them directly into my program to verify them.

I personally think it would be interesting if we had a nightly-only/unstable pre/post conditions in the std library. Then one could take the commit of the compiler that corresponds to a stable release and verify against that. That is the overhead I seem to be bumping my head against whenever I try to verify some rust code at least.

[pjmlp]

Since learning Eiffel in the 90's I keep looking forward for them to become mainstream, beyond the typical assert like statements.

So far we had annotations in Java (which required additional tooling and never took off), .NET (hidden behind enterprise license, thus hardly adopted), D (which suffers from adoption), Common Lisp (nice, but again adoption issues), Ada (again the language adoption), C++26 (if they actually land, and only as MVP)

Almost 40 years later, and still no good story for DbC.