Hacker News Reader

Comment by thomasahle | Hacker News Reader

This is actually really cool. They tried to verify Timsort as implemented in Python and Java using formal methods. When it didn't seem to work, they discovered that there was actually a missing case in both implementations, which could lead to array out of bounds exceptions.

Really shines as an example of how important proof is in computer science.

View on HN

In the Haskell community there is a tool called QuickCheck [1]: it is able to generate inputs based on preconditions, and you provide a function to verify the postconditions.

I am not sure why these kind of testing methods aren't used more often in other communities, since it makes it really easy to catch corner cases; in the Haskell world, at least, using QuickCheck is somewhat pervasive.

[1] https://wiki.haskell.org/Introduction_to_QuickCheck2

EDIT: I have never done this before, but could anyone explain why I am being downvoted? I wasn't making the claim that this is a substitute for a formal proof, I was merely adding this information to the discussion since it seemed relevant.

Just FYI for anyone who's interested, but there's a Swift implementation of QuickCheck described in this book:

http://www.objc.io/books/

It's very minimal, but the chapter outlines what you'd need to do to make it more complete and get it on par with the Haskell version. There are also a few versions on GitHub too.

At a guess: A lack of practical ways to perform such checks without extensive extra knowledge and annotation as seen in the article. A large factor is likely that Haskell is pure by default - something that is reasonably rare in many languages (where a method likely reads (or mutates) state from instance variables or even globals).

I think it also has to do with Haskell's type system. Quickcheck is able to "discover" the bounds within any arbitrary type can operate, and thus makes generating random values within these bounds fairly easy.

Eh, you still have to write instances of Arbitrary. And often those instances are not great; wayyy to many libraries are tested with Arbitrary String instances that only generate ascii, for example.

It wouldn't catch this bug. The algorithm works for lists of size less than 2^49.

There's a difference, though: QuickCheck randomly tries a large-ish number of possible inputs to try and disprove a postcondition, whereas formal methods prove the postcondition for all inputs. Practically, if the number of possible inputs is huge compared to the number of failure cases, it's unlikely that QuickCheck will find it. I strongly suspect - and this would be an interesting experiment - that QuickCheck wouldn't have found this particular bug, since Timsort has been in use for years without anyone noticing it.

What about AFL?

What's AFL?

American Fuzzy Lop (http://lcamtuf.coredump.cx/afl/), a fuzzer which instruments programs at compile-time to help find interesting inputs faster than brute-force fuzzing.

It may have indeed found a bug in TimSort, since it's more apt at exercising branches, but I think AFL is C/C++ only.

I'd say that QuickCheck would have a hard time coming up with a failing test case since the input needs to be rather large to trigger the bug.

It would be interesting to see if QC would find data easily that brake the implementations or require some tuning in the way it generates test data.

And sorry, I have downvoted you by mistake when I wanted to reply.

I am trying (with some success) to get QuickCheck used in the Rust community.

Listing my projects that us QuickCheck would be cheating, so I'll link projects that aren't my own. The most impressive, by far, is this linear algebra library: https://github.com/japaric/linalg.rs/tree/master/tests --- Just pick a file at random and look for `#[quickcheck]`. :-)

Here's some fancy testing for a "concurrent, lock-free, linearizable, insert-only, sorted map": https://github.com/danburkert/pawn/blob/1afe50c618a733de63b9...

Another: https://github.com/apasel422/tree/blob/6656140c44687793e31ae...

And OK, I'll stop now, but you can see more here: https://github.com/search?q=extern+crate+quickcheck&type=Cod...

The use of these sorting functions is already orders of magnitude more than random testing would cover. This is a very rare failure, only affecting huge arrays, arrays so large that quickcheck would not even test it.

In C# there's a similar tool called Code Digger[1]. It analyzes all possible branches of a function and generates input to cover all of them, this includes not only your own "if's" but also branches inside library functions and stuff like divide by zero and dereferencing null pointers. It's really impressive and can even generate strings and arrays with data that causes a different branch to be taken.

Sadly i found it to be no more than that, cool. On real life code it's not useful. Real code usually has a lot of mutable state, this tool works best with pure functions. Real code does pretty complex things like parsing xml, that takes too much time to analyze for these tools. Bugs in real code are not always exceptions or error codes returned, maybe you assigned foo.x to bar.y instead of bar.x, maybe the sort doesn't crash but your numbers came out unsorted, how would the tool know that's a fault? Real bugs happen across threads or even modules running on different machines. And the list goes on. Only if you have functions that are very pure and mostly work with simple data types, few strings and lists, it can be good to use as startng point for input to a test suite but doesn't replace it fully.

[1] https://visualstudiogallery.msdn.microsoft.com/fb5badda-4ea3...

Here is an implementation of Timsort in Haskell that also exhibits the bug:

https://github.com/timjb/haskell-timsort/commit/d9c3e1e454c7...

I find interesting that this Haskell version of Timsort also exhibits the bug, despite Haskell having a type system more advanced than Python or Java. This is a reminder that type checking is not a magic bullet, and is hardly enough to prove a program correctness. Formal proofs and whole program static analysis are still necessary, with or without an advanced type system:

http://www.cl.cam.ac.uk/~srk31/blog/2014/10/07/

Reply on news.ycombinator.com