[pmarreck]

If you're going to go Haskell, why not go all the way to Lean 4 and get mathematical provability along with reasonable speed and type-safety?