[switchbak]

Don't need to write _type_ tests (like you would in a dynamic language). Having strong typing doesn't magically do formal validation on your logic. Leaning heavily on types is good practice, but that doesn't eliminate most of the high value tests you'd have to write.

[mananaysiempre]

Haskell's QuickCheck, AFAIK the first prominent implementation of property-based testing, gained its popularity partly because it eliminated a good part of the tedium by inferring the sampling strategies from the types (which in idiomatic Haskell are, due to liberal use of opaque type synonyms, often quite a bit more specific than in any other non-dependently-typed language I've seen). Which does not free the programmer from writing down the properties themselves—in that respect your objection is valid—, but IME still makes it quite a bit more ergonomic than e.g. Python's otherwise functionally equivalent Hypothesis.

[switchbak]

You'll find no argument from me there, property based testing has been a real game changer for me. I imagine it would have a fraction of the value without being able to leverage the type system to a great degree.

[tluyben2]

> Having strong typing doesn't magically do formal validation on your logic

There are plugins for Haskell and dependently typed languages that go much further in the ‘if it compiles, it is formally validated’, but that’s a lot more work; there is a trade-off for now or you will be stuck. Your ‘run of the mill’ tests also don’t formally validate your logic (not even close usually). Our types, even if static, are usually too loose and our type systems not powerful enough; writing tests helps to close the gap between practical and theoretical but a lot more can be done semi-automatically (and will be I hope).

[nequo]

> There are plugins for Haskell and dependently typed languages that go much further in the ‘if it compiles, it is formally validated’

Yes, Lean 4[1] is shaping up to be a Haskell-inspired dependently typed language with monadic IO etc. that can also prove theorems for you. Still a work in progress but looks very exciting.

[1] https://leanprover.github.io/lean4/doc/

[epgui]

See also:

- Idris (https://www.idris-lang.org/)

- Agda (https://wiki.portal.chalmers.se/agda/Main/HomePage)

I'm really excited by progress in this space! :)