4 ms·

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 i

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 and not that i would be nearly useless because i wouldn't be able to prove the most basic every-day functions. 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)

tom_mellior 10y ago
> 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.
bbcbasic 10y ago
Liquid Haskell is worth a look
- LeanderK 10y ago
  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! [0] http://goto.ucsd.edu/~nvazou/thesis/main.pdf http://goto.ucsd.edu/~nvazou/thesis/main.pdf

tom_mellior 10y ago

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

bbcbasic 10y ago

Liquid Haskell is worth a look

LeanderK 10y ago
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! [0] http://goto.ucsd.edu/~nvazou/thesis/main.pdf http://goto.ucsd.edu/~nvazou/thesis/main.pdf