5 comments

[ 65.0 ms ] story [ 579 ms ] thread
Just so I understand this correctly, this is a tool where, if you provide it a program, it will use reduction/rewrite rules to find a simpler program that exhibits some given behavior?

In practice, how is this applied? Do compiler developers essentially use something similar to quick check to generate breaking programs and then use this to reduce those programs to a minimal form, or am I missing something else altogether?

I agree it looks similar to QuickCheck shrinking. Isn't necessary limited to compiler writers though; e.g. I can imagine a big numerical calculation (like a physics simulation), giving NaN outputs. This could presumably home-in on the problematic step (given an appropriate test script).
Yes. An example (in the associated paper) is to create a minimal reproduction of a crash so it's easier to debug.