Comment by kreetx

Some type systems (e.g, Haskell) are closing in in becoming formal verification languages themselves.