>it's not either value or business invariant. I'm not convinced as long as you're not writing proofs in dependent-type languages like Idris. Types are proofs i

>it's not either value or business invariant. I'm not convinced as long as you're not writing proofs in dependent-type languages like Idris. Types are proofs in OCaml as well, you don't need dependent types to have Curry-Howard correspondence. You could even prove stuff in Java. And you can ensure invariants with types in OCaml well enough.