Actually, using Ada + SPARK, there are many static properties that can be verified which would be unverifiable in Haskell, and would be awkward to verify even

Actually, using Ada + SPARK, there are many static properties that can be verified which would be unverifiable in Haskell, and would be awkward to verify even in Agda or Idris. But you've got your mind made up already -- please just enjoy your tools, and let others enjoy theirs.