> This is where I stop understanding how the rest of the world can work at all. Without some rigorous tools I just do not see how one can get such things right.

> This is where I stop understanding how the rest of the world can work at all. Without some rigorous tools I just do not see how one can get such things right. Well, sure, spend weeks of trying out test cases, printing out the structures, manually check everything (in the testing world this is known as writing lots of “oracles”), try at great pains to find out the reason for wrong results, guess what program change will fix the problem, and start again. Stop when things look OK. When, as Tony Hoare once wrote, there are no obvious errors left. Most businesses put their data in a DBMS, so you have integrity constraints "to ensure database consistency with the business rules or, in other words, faithful representation of the conceptual model of reality."[4] The relational model is both complete and a lot easier to understand than using the predicate calculus directly. The other shortcoming of any language's invariants is that it lives in your source repo. As coders, we often forget that your production data represents contracts with customers, and you have to take account of the real data when migrating your business rules. That's why the M is in DBMS. More directly answering the question, most languages can employ property tests [1][2][3] that, very closely to how Eiffel does it, allow you to specify the precise invariant and validate it under randomly generated tests. But, honestly, a great deal of code, even math heavy code, doesn't have nice general invariants. Real functions dealing with business logic and bugs are piecewise and messy. And then that only covers the handful of functionality that is even remotely expressible in mathematical form. You still have the user interface to deal with, dependency management, your entire deployment story, and all the problem extant between chair and keyboard. Technology can't substitute for the grunt work of testing, testing, actually using your system and talking to your customers. [1]: https://hackage.haskell.org/package/QuickCheck https://hackage.haskell.org/package/QuickCheck [2]: https://hypothesis.readthedocs.io/en/latest/ https://hypothesis.readthedocs.io/en/latest/ [3]: https://github.com/HypothesisWorks/hypothesis-java https://github.com/HypothesisWorks/hypothesis-java [4]: http://www.dbdebunk.com/2017/06/what-meaning-means-business-rules_11.html http://www.dbdebunk.com/2017/06/what-meaning-means-business-...