Comment by throwaway2016a

Non click-bait title:

"Using Coq to write formal proofs of an image browsing app written in Haskell"

While this seems interesting, in this type of application what benefit does this have over, say... unit and integration testing?