Support for Pre, Post conditions and invariants

[pjljvandelaar]

Hi Haskell 2020,

After using Haskell a lot, I am now programming in Ada and Spark. Despite that SPARK is non-functional, the tooling (using problem solvers like Z3 and cvc4) is still able to prove correctness of functions and procedures, and thus eliminating some needs for testing. Since Haskell is a pure functional language, the proofs should be easier imho. However, pre-, post-conditions and invariants can't be expressed in the haskell language: they can only be added in comment. See e.g. https://github.com/TorXakis/TorXakis/blob/develop/sys/valexpr/src/Boute.hs

Please consider adopting a similar approach to SPARK to specify pre- and post-conditions and invariants in Haskell. Even when tooling can't prove the pre-, post- conditions and invariants, they can still use it as a basis for testing.

Some example

divMod :: Integer -> Integer -> (Integer, Integer)
divMod m n
  with Pre : (dinstinct n 0)
          Post: ( (let ((r (fst divMod'Result))(q (snd divMod'Result))) 
                     (and (<= 0 r (- (abs n) 1)))
                           (= m (+ (* n q) r))
                   )

add :: Integer -> Integer -> Integer
add m n
   with Invariant: add m n = add n m
           Invariant: add m 0 = m
           Invariant: add 0 n = n

Note that the invariants are comparable to the properties of property based testing.

[FranklinChen]

@pjljvandelaar How does Liquid Haskell https://ucsd-progsys.github.io/liquidhaskell-blog/ suit your needs? It uses SMT.

[pjljvandelaar]

Great to see that the features I propose are already implemented. For me this increases the urgency for standardization. Not only to prevent different dialects, but also to ensure other tools include pre, post conditions and invariants. To give some examples, refactoring tools also change these conditions; documentation tools are nicely layouting these conditions; and dependency tools acknowledge dependency needed for these conditions.