[jcgrillo]

> no good reason for you application environment not to query the invariants from there and test or prove your code around them

As a developer who primarily builds backend web applications in high level languages like golang and java I run the risk of sounding ignorant talking like this but.. I'm led to believe lower level systems and embedded software has a lot more invariant preserving runtime asserts and such in it. The idea being that if an invariant is violated better to fail hard and fast than to attempt to proceed as if everything is alright.

[marcosdumay]

Hum... I'm not sure we are talking about the same thing. Of course system and embedded software won't have invariants stored in a database, the comment isn't about them.

But, there isn't a faster way to fail to an invariant than to prove statically that your code fails it, or to test it before deploying. I don't really understand your criticism.