Blog articles/Testing

Type checking for correctness

• Can your type checking system do this?

Testing, correctness and proofs

QuickCheck

• Introduction to QuickCheck
• QuickChecking a window manager
• Robustness and QuickCheck
• Parsec Parser Testing with QuickCheck
• QuickCheck : Why Testing code should be Laissez-faire

HUnit

• On Unit Testing and Type Safety
• Getting started with HUnit

Catch

• Does XMonad crash? On proving pattern coverage with Catch
• Preconditions on XMonad
• Equational Reasoning in Haskell

Proofs

GADTs

• Developing Programs and Proofs Spontaneously using GADT

Coq

• Strong specifications in Coq: the type says everything

Isabelle

• Proving Haskell correct with Isabelle/HOL

Related work

• See the section on theorem provers

Further reading

• Research papers on testing, proofs and correctness