> type systems can be regarded as a weak form of formal verification

Depends on the type system, right? I was recently looking at Idris which is a general purpose programming language but apparently can be used for proofs.