Stream: t-compiler/wg-nll

Topic: polonius proptests


Jake Goulding (Dec 31 2018 at 17:11, on Zulip):

(that is, the piece of code to generate a random set of valid facts seemed not immediately obvious but maybe it's not that hard)

I've found that this is, hands-down, the hardest part of property-based testing.

That being said, we programmers implicitly do this kind of thinking all the time but don't explicitly encode it.

Jake Goulding (Dec 31 2018 at 17:14, on Zulip):

"Oh, the first argument has to be less than the second argument"

Jake Goulding (Dec 31 2018 at 17:16, on Zulip):

The other thing that I've found super useful is to use these types of tests to exercise variants of algorithms: "for every input, the SIMD-accelerated code must have the same results as the naive code"

This might be highly useful in this case as you could write "stupidly obvious" code that isn't as efficient as the :frog: but it's easy to verify it's correct.

centril (Dec 31 2018 at 17:19, on Zulip):

are we talking about property based testing in general or the proptest crate specifically?

centril (Dec 31 2018 at 17:23, on Zulip):

PBT usually runs along the lines of 1) roundtrip (encode . decode = id, decode . encode = id), 2) test against known to be correct algorithm, 3) running a verification algorithm on a decision algorithm, e.g. is_sorted on the result of sort + then also checking that its a permutation

lqd (Dec 31 2018 at 18:00, on Zulip):

some of my favorite PBT strategies are from https://fsharpforfunandprofit.com/pbt/

centril (Dec 31 2018 at 18:08, on Zulip):

funny :P; ooh! diagrams are a nice strategy -- the aspiring category theorist in me likes this

lqd (Dec 31 2018 at 18:09, on Zulip):

the inputs seem a bit tough indeed to generate here, esp some of rustc’s liveness (if we need those facts) but some relations are easier than others; the test text parser already shows some of these validity rules / fact generation —definitely interesting

centril (Dec 31 2018 at 18:09, on Zulip):

@lqd yeah graphs are usually hard to generate I find

centril (Dec 31 2018 at 18:10, on Zulip):

@lqd have you tried the proptest crate?

lqd (Dec 31 2018 at 18:10, on Zulip):

(even reusing rustc might have been an option :)

centril (Dec 31 2018 at 18:10, on Zulip):

I'm biased (since I wrote some of that code...) but it's pretty ergonomic to use

lqd (Dec 31 2018 at 18:11, on Zulip):

only quickcheck myself but I think niko has added some tests using it to datafrog

centril (Dec 31 2018 at 18:11, on Zulip):

/me looks

centril (Dec 31 2018 at 18:13, on Zulip):

cool

centril (Dec 31 2018 at 18:14, on Zulip):

@lqd we're working on a book + shipping #[derive(Arbitrary)] which should remove some of the boilerplate

lqd (Dec 31 2018 at 18:14, on Zulip):

nice!

lqd (Dec 31 2018 at 18:15, on Zulip):

I hope we’ll use it more then :)

centril (Dec 31 2018 at 18:15, on Zulip):

:P

centril (Dec 31 2018 at 18:17, on Zulip):

@lqd it would be nice to get CoArbitrary to work as well to proptest some HoFs and such; I spoke to Koen about it a while back but it was sorta tricky to implement without GADTs so I put it on hold

lqd (Dec 31 2018 at 18:18, on Zulip):

:)

Jake Goulding (Dec 31 2018 at 20:09, on Zulip):

I still love the post about using QuickCheck to test an entire C application

centril (Dec 31 2018 at 20:09, on Zulip):

@Jake Goulding is that John's article?

Jake Goulding (Dec 31 2018 at 20:11, on Zulip):

https://pdfs.semanticscholar.org/76c7/ddcaadee1fc0b475df59c08bf0700313586d.pdf ? Seems likely

centril (Dec 31 2018 at 20:13, on Zulip):

Ah; nice one -- I really like this paper: https://dl.acm.org/citation.cfm?id=2364516

Jake Goulding (Dec 31 2018 at 20:32, on Zulip):

That link doesn't provide a way to read the article without paying, is that correct?

centril (Dec 31 2018 at 20:33, on Zulip):

@Jake Goulding yeah sadly; here's a talk Koen held about it: https://www.youtube.com/watch?v=CH8UQJiv9Q4

centril (Dec 31 2018 at 20:33, on Zulip):

implemented here: http://hackage.haskell.org/package/QuickCheck-2.12.6.1/docs/Test-QuickCheck-Function.html

centril (Dec 31 2018 at 20:38, on Zulip):

@Jake Goulding Fortunately I found it in my stash :P p73-claessen.pdf

lqd (Dec 31 2018 at 22:09, on Zulip):

cough sci-hub cough

Last update: Nov 21 2019 at 13:30UTC