To add to this, you cannot have dependent proofs 'easily' in Haskell, but you can use LiquidHaskell for proofs!