> DbC is the Policy (i.e. what/why) and Asserts are the Mechanism
The ideal way to do runtime-checked DbC is not with simple asserts, it's with proper first-class preconditions and postconditions at the language level.
It wouldn't be nice to have to manually ensure that both old and new states of variables are in-scope for postcondition checking. I can imagine that being not just tedious, but error-prone.
> An Assert merely validates the state of a program at a particular point during execution.
Some aspect of the program's state, yes, and hopefully that's all it does.
Interesting to think about the edge-cases here though. Depending on the language, it could accidentally side-effect, or even invoke undefined behaviour, and so actively derail the program. Can't blame DbC for that though, that's a question of language safety.
> You use it to steer the program to go through only the correct subset of the state space of the program
I'm not sure I follow here. You don't use asserts to steer flow-control, you use them to check aspects of program state.
> You could do this pre/post every executable statement (i.e. write proof of correctness)
That doesn't constitute a proof of correctness, no more than last time you and I discussed this. [0] Depending on the language, it wouldn't even necessarily prove the correctness of that particular trace, as you haven't proven that you haven't accidentally invoked undefined behaviour.
You hold a minority opinion on this, please stop presenting it as settled fact.
> The point is that when using asserts you think about correctness w.r.t. specifications and nothing else. To think of it as simply validating arguments or in terms of effects on optimization is quite the wrong thing to do.
I'm not sure why you'd think I don't already know that.
[0] https://news.ycombinator.com/item?id=44675668