A remarkable post introducing a GHC plugin that proves your programs obey laws: https://www.joachim-breitner.de/blog/717-Why_prove_programs_equivalent_when_your_compiler_can_do_that_for_you_