search

mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.
https://code.google.com/p/epigram
MIT License
48 stars 7 forks source link

RFC: Quickchecking #34

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
This is more of a poll than a feature request. I will re-send to the mailing 
list if I cannot reach a critical mass here.

Right now, we have something like 9246 loc (only counting the "> " lines). 
Apart from the ./tests directory, we have absolutely no tests on individual 
components of the system and, worse, absolutely no invariant stated. 

I think that just stating the invariants would already be a first and important 
step. I find it amusing that being wannabe mathematicians, our code is less 
specified than an EE-undergrad's code...

I suspect that the major hurdle with QuickCheck will be to randomly generate 
types and terms inhabiting these. Then comes the issue of generating types (and 
the associated term) of a particular form, such as an elimination principle. 
However, for a start, we could hard-code a few of them.

Does anybody think that this is feasible/useless/...?

If there is public interest, I can push a first go I had on ProofState.

Original issue reported on code.google.com by pedag...@gmail.com on 11 Aug 2010 at 5:49

GoogleCodeExporter commented 9 years ago

Original comment by pedag...@gmail.com on 11 Aug 2010 at 6:54

GoogleCodeExporter commented 9 years ago 
I agree that stating more invariants explicitly and introducing more extensive 
tests would be worthwhile. Random generation of terms seems like more trouble 
than it's worth; perhaps we could create a corpus of type-term pairs instead. I 
am not really familiar with Haskell testing frameworks, so is QuickCheck good 
for this kind of testing or should we look at something else?

I would be interested in seeing your ProofState tests. If you don't want to 
push them yet, you could always darcs send them to me.

Original comment by adamgundry on 1 Sep 2010 at 7:55