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.
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.