As far as I can tell, a static, strong typing system sets a baseline of assumptions that you must further verify as an exercise to the business logic programmer

As far as I can tell, a static, strong typing system sets a baseline of assumptions that you must further verify as an exercise to the business logic programmer. With more dynamic, weak type systems, more tests must exist to achieve a similar level of guarantees. For me, this all seems vaguely similar to when people argued about garbage collectors v. manually managed memory and it's become more that you've traded one set of problems for another, and as far as pragmatic engineering goes I think that's perfectly fine as long as we're better equipped to handle the new problems. But yes, I'll take strong tests mostly because I can only spend so much time verifying that a type system aligns with my business logic (granted, QuickCheck is neat but requires a high price in flexibility of language choices) and I'd rather take the approach of weaker type systems with partial correctness than the oftentimes all-or-nothing demands of a rigorously structured business framework within a mathematically oriented language. This is very much a "worse is better" sort of approach to me and I argue it's why imperative and OOP languages will continue to dominate in anything outside academic programming.