You're right, I should amend this statement: > Type checking (safety) is only one subcategory of proofs Type checking as provided by Rust, Haskell, etc. only

You're right, I should amend this statement: > Type checking (safety) is only one subcategory of proofs Type checking as provided by Rust, Haskell, etc. only covers a subset of possible proofs. Liquid Haskell goes further to increase the range of possible proofs it covers through type checking by using automatic theorem provers.