Those of you who’ve done both: what do you like about statically typed languages (vs. dynamic)?
-
Of course some things are unprovable in any type system. And tests to prove trivial things are really irritating and unproductive to write. So it’s worth having a mix.
That wholly depends on the type system. Nobody writes tests for this type, even in an undecidable system: forall p. p -> p because that would be foolish. You have a proof and tests are redundant. Bob's argumentation consistently depends on rubbish type systems and side-effects
