Re:Coq 8.6 is out
by tom_mellior on Wednesday December 14, 2016 @07:56PM
(#13181340)
> OK, so if i want to build a program that proves my haskell code with a similar ease as using quickcheck[0] it would be possible, its just that nobody has done it yet
Yes, kind of. For certain values of "similar ease" and "Haskell". AFAIK Agda is pretty much Haskell, but its proving part is not all that automatic. On the other hand, Isabelle has a lot of proof automation (and includes an implementation of QuickCheck that it applies automatically to every property you state when you start proving it!), but its own variant of functional programming is not exactly Haskell. I think you can extract Haskell programs from it, though.
> I would guess an database of previously proved lemmas for all the used libraries would help
It may help, but it may also confuse the proof search if it gets lost in a sea of irrelevant lemmas. Which is what I was trying to say above, I never said anything about recomputing stuff.
Liquid Haskell is worth a look
i was not aware of what's going on with Liquid Haskell! This dissertation[0] just came out and looks like to be exactly what i had in mind!
I would guess an database of previously proved lemmas for all the used libraries would help, so that you don't have to recompute everything.
[0] quickcheck is an awesome library that generates unit-tests for specified properties (like: "for all lists s: length(sort(s)) = length(s)", i would then just generate a few hundred lists and check whether the property got violated)