I agree with your sentiment - why bother testing something that we can get the compiler to prove, once and for all? However, <i>in Java</i>, a typeful model of a program&#x27;s specification is bound to be:<p>(0) Imprecise, because of the holes in Java&#x27;s static safety. You can establish a convention that statically unsafe features are verboten, but it will remain just that - a convention.<p>(1) Verbose, because Java can&#x27;t express even the simplest ideas without using at least 5 classes: Finite case analysis? Visitors. Higher-order functions? Strategies. Persistent data structures? Memento. Things don&#x27;t get better if we move to a higher architectural level: Embedded DSLs? You need a separate class for each production rule in your abstract syntax. Type-safe database queries? Java has no structurally typed records, so you need to make a custom POJO class for every query that returns different columns.<p>These things are incredibly unpleasant to deal with, and while it might be true that &quot;unpleasant work builds character&quot;, I don&#x27;t think it should come as a surprise that some people say &quot;enough is enough&quot;, and seek alternatives that minimize or at least reduce their pain (like dynamically checked conformance to a schema), even at the cost of sacrificing some type safety (dynamic checks can&#x27;t enforce higher-order invariants).