The "ideology" video linked at the end of the article was also instructive for me, by framing the issue in other terms. Both tests and types are proof of correc

The "ideology" video linked at the end of the article was also instructive for me, by framing the issue in other terms. Both tests and types are proof of correctness; tests are proof by example, types are proof by category. The architectural analogy in my head is that types are vertical and horizontal beams, while tests are diagonal bracing. The interlocking of the two is what makes the overall structure rigid.