Only want to say

[Timon Gehr]

On 12.01.21 18:04, H. S. Teoh wrote:
>  > they should be in a
> form that's readable and understandable to the user.
> Any other conditions that don't fall in that category belong as asserts in the
> function body, not in the contract.

If an assert fails in the function body, the function has a bug. If an 
assert fails in the in contract, the caller has a bug. I understand that 
some people don't take this very seriously for pragmatic reasons, but 
one should at least be aware that this is supposed to be the convention.

Modular correctness is great, runtime checking maybe not so much.