DRMacIver

> Smarter in what way?

Better at generating values that exhibit interesting behaviour in tests. QuickCheck style testing mostly only works well because it turns out that there are a lot of bugs that are relatively "dense" in the search space of tests, and doesn't do very well at finding hard to reach bugs. This means that some bugs are found with very low probability, which is bad both because you want to find them reliably and because it means that even running your tests for longer is often not enough to find interesting behaviour.

(ETA: This mostly applies to Haskell QuickCheck and derivatives. I believe the Quviq Erlang QuickCheck has had a great deal of hand tuning of its generators to get better behaviour, so its data generation is probably strictly better than Hypothesis's in many cases right now. I'm trying to get a generic mechanism for improving things without requiring this hand tuning, so hopefully at some point I'll be able to reverse that situation)

Security-oriented fuzzers do a lot of clever things to actually determine the shape of the search space and adapt to it so that they can take advantage of the structure of the program under test so that running for longer gives them more power than just repeatedly trying the same thing over and over again. I'm hoping to incorporate some of those ideas into Hypothesis but don't currently.

> What makes QuickCheck's support for this makes it work less than ideal?

Mostly that it plays very badly with shrinking (this is better but still not good in test.check and friends) and the API for it is on the clunky side.

> What do you mean by not having to "touch" the values it generates?

In classic quickcheck, the shrink API is based on taking a value and replacing it with a simpler version of itself. This means that if the value has been mutated (which is mostly not a problem in Haskell, but can be if you're using ioProperty, and is definitely a problem in QuickCheck ports to impure languages) then you run into problems. e.g. a test that appends an element to a variable sized array argument can get the shrinker into an infinite loop.

It also means that QuickCheck is limited by the type constraints on the generated values. You can't e.g. do duplicate detection because you aren't constrained to generate values on which that is meaningful.

In Hypothesis in comparison everything is based off its IR, so it can do manipulations and comparisons on that, and it doesn't matter what type the generated value is.

(Hypothesis also can't do perfect duplicate detection because it has the problem that many IR values may map to the same value, but its duplicate detection still seems to be mostly good enough in practice)

Internally, Hypothesis is built on a core engine called Conjecture, which looks more like a byte stream fuzzer than anything else. Hypothesis data generators are then effectively parser combinators on top of that fuzzer.

This gives Hypothesis a lot more freedom to generically manipulate the data than QuickCheck has, because it has total control of a concrete representation of it.

As a result:

* Specifying a data generator is a much more declarative process - Hypothesis largely handles size/distribution issues itself.

* The fuzzing nature of Hypothesis means that it can do much smarter generation than a normal QuickCheck (though this is more potential than actual right now. The current fuzzer is "pretty good". I'll be starting a PhD soon where I hope to work on making it amazing)

* Shrinking is just a built in part of the process and users never have to define their own shrinker.

* All examples (both pre and post shrinking) can be serialized because the IR is just bytes, so Hypothesis can replay failing tests automatically without rerunning the shrinking process. This matters both because shrinking tends to be slower than generation in most QuickChecks, but also because in general shrinking is subject to "slippage" where the bugs you find after shrinking are different from the bugs you started with.

* Because you can just keep drawing data from the stream, Hypothesis tests can be much more interactive than normal QuickCheck (which does support mixing test execution and generation, but it doesn't work especially well).

* Because Hypothesis never needs to touch the values it generates, Hypothesis is much better for mutable data than the approach most QuickCheck takes.

* I haven't actually done this yet, but Conjecture is deliberately designed to be quite C like, so "at some point" it will become possible to rewrite the core in C (more likely Rust) and then new Hypotheses will spring up everywhere because 90% of the work can be done by writing bindings to a C library. QuickCheck's approach on the other hand is inherently very tied to the semantics of the host language.

The property-based testing libraries for some dynamic languages (test.check for Clojure, the various Erlang ones including QuickCheck) have some of these features, but I think they're more naturally supported in the Hypothesis model, and the Hypothesis model has a lot more room to grow.

> Also, by "supporting Hypothesis", you mean "giving money to DR MacIver", right? This is not completely clear from the post.

It's specifically in the form of contracting me to develop some features rather than a donation of money - support for testing with Pandas, and improving the existing numpy support to a lesser extent (mostly with a goal of providing a more solid foundation for the Pandas work).

> Hypothesis is a quickcheck port to python

If you'll pardon the pedantry (I think the distinction matters, honest), Hypothesis isn't really a QuickCheck port. It started out life that way, and it can be used in a way that that is pretty compatible with QuickCheck, but implementation-wise it's very different and it has a bunch of interesting non-QuickCheck features.

I totally agree that this is great news though, and I'm very grateful to Stripe. :-)

This piece by Dr Jen Gunter provides some better perspective on this study I think: https://drjengunter.wordpress.com/2016/11/01/new-study-doesn...

Short version: The study is interesting but the early termination is largely ethics review working as intended and does not mean that all research into this method is terminated or that the results weren't promising.

I might not say that the use of any language is a bad idea, but I'm definitely going to say that basing a language choice on a general and uncertain impression derived from my extremely limited, biased and anecdotal sampling as an end user is a terrible idea :-p

ETA: The point of that anecdotal impression was not "This is definitely true" but "Given that this is my general experience it would be surprising if the actual trade offs experienced in practice were such that static typing was regularly a clear winner", which I feel much happier supporting on an impression than "You should do this".

> I don't think the OP would claim TypeScript is a bad idea

Confirmed.

TBH there are very few languages that I'd claim were a bad idea. The point I'm making is not "Statically typed languages are a bad idea" it's "If you think statically typed languages are going to make software correctness magically better then you're going to be disappointed".

It might be based on false information - I'm a bit out of touch with Java development. I'll remove it.

> Most Smalltalks didn't really have great code completion (or code completion at all),

Ditto most statically typed languages.

> The fact that it's hard to write language tools in general doesn't change the fact that it's way harder to write an IDE for a dynamic language than it is for a static one.

It doesn't, but the fact that there's nearly as much variation within statically typed languages in terms of how difficult this is to do as there is between statically and dynamically typed languages does. And this only gets worse as we move to the sort of languages that the static-types-for-correctness people advocate for.

> Code completion is a fundamentally harder (if not impossible) problem with dynamically typed languages

Code completion tools originally came out of Smalltalk. It's relatively doable if you can attach to a running process that has dynamic access to your code.

So that's "not necessary". It's also not sufficient: Most statically typed languages simply don't have this sort of tooling because it's very hard to write, and advanced type systems make it even harder.

> Being able to hit . and get a reliable list of things I can do is worth many millions of dollars to me.

...and mostly is possible because of the many millions of dollars that were thrown into developing it rather than the type system. Quality of tooling has much more to do with the amount of money invested in it than whether the language is statically typed.

But this isn't a post about static vs dynamic typing as I said right at the top. It's a post about the effect of static typing on software quality.

FWIW, rantly (https://github.com/abargnesi/rantly) rather than propr seems to be the most active and usable Ruby property based testing library.

(I maintain a list here: http://hypothesis.works/articles/quickcheck-in-every-languag...)

For certain values of works, that's true. It will take a long time and won't produce very good results.

structureshrink more or less came out of frustration with what a bad job most of the existing shrinkers do. In particular the algorithm that lithium uses is more or less structureshrinks last ditch "Welp, everything else has failed, might as well try this" approach.

Technically they're an earlier design than the ones found in the Milky Way by the time of the show.

But, um, honestly I hated Universe and didn't watch much of it, so it's not very surprising that this doesn't manage to be compliant with it.

I think you're confusing episodes. In his first appearance he mentions that he's allergic to citrus. The "I love lemon chicken" incident comes from Carter's visit to a parallel universe when she's experimenting with the merlin device in a later season.

...I'm really embarrassed that I know that from memory.

The basic conceit in writing this story is that when you only have access to an area of physics through poorly understood reverse engineered xenotech, a lot of arbitrary constraints imposed by the tech start to look like physical laws.

One would certainly hope this to be the case, but it's hard to watch SG1 and get the impression that the ancients had much of a concept of defensive design.

About a third of them aren't from any episode, including that one.

Yeah, this piece has been described as Stargate/Hypothesis crossover fic before.

> Temit was an ascended being, because surely near-omniscience is the only explanation

Any sufficiently advanced QA department is indistinguishable from ascension.

> for his ability

Stop misgendering my werewolves. >:(

> Anyhow, one minor issue: the gates were thought of by a guy named Amelius the night before they left the Alteran Home Galaxy, long before they ever reached Earth. :)

Yeah, I had the timeline slightly wrong for how long it took them to get to earth. In my defence there's no evidence of them making Stargates pre Milky Way (he came up with the idea in the Ori home galaxy but they then spent a few thousand years looking for somewhere to settle), and we don't know how long the Alterrans lived, so it's just about plausible, but it's a bit of a reach.

Most libraries found in the wild are kinda crap, because as an industry we have a massive problem where most of our stuff is built on free labour that people have performed in their spare time to scratch their own itch.

Using libraries is still generally a good idea, but its effect on software correctness is a bit of a coin toss.

> I don't think that's a fair analogy. At this point, I believe we have pretty good ideas that make it possible to write correct software. Most impressively, there has been progress on creating a completely verified C compiler named CompCert: http://compcert.inria.fr/. This really means "completely verified"---they formalized the semantics both of C and of assembly, and used an automated theorem to prove that the semantics of the generated assembly are the same as the semantics of the source code.

Note that Compcert has had bugs found in it too. Compcert has a verified core, but it's not a fully verified piece of software.

It's still a lot closer to bug free than almost any other software out there.

It's pretty easy to do this sort of thing in Hypothesis. You can also use [the support for stateful testing directly](http://hypothesis.readthedocs.org/en/latest/stateful.html). I find there's still a place for more granular tests that look more like your classic property based tests with a bit more imperative state floating around though.

Have you seen the talk I did about using it with Django? http://www.drmaciver.com/2015/06/hypothesis-for-django/

We're all still figuring out the details, but this sort of testing definitely works for testing your applications as well as your algorithms.

ETA: Oh, and thanks for the kind words. :-)

They're mostly the hobbyists. They're also the people you encounter in other languages (e.g. Scala) telling you how much better this all would be if you just understood Haskell. Unfortunately, due to the relative lack of success of Haskell in industry this is the majority of the people who consider themselves Haskell programmers, and certainly the majority I encounter on the internet.

> I think you're equally missing the point– for serious Haskell programmers, using a monad to structure computation for a CRUD app is nothing to write home about. Having personally written quite a lot of CRUD code with Haskell, I have never thought "Gee, I wrote this with a monad. I deserve a back pat."

Missingthepointception!

It's almost like I didn't explicitly point to this as a phase most serious Haskell programmers grow out of right in the goddamn article.

> You could just as well argue that laying out object class hierarchies and using inheritance is "[solving problems] that have nothing to do with what you’re actually trying to achieve."

Could, indeed semi-regularly do. I actively dislike solving problems with inheritance.

I also actively dislike people missing the point. The problem is not "using programming to solve problems". The problem is letting the novelty of the programming you're using to solve problems con you into thinking you're doing something more clever than you actually are.

The difference is, I know when I'm not being funny.

Personally I'd like to embrace the power of 'and'. :-)

As someone who is going to be trying to make a living from his open source work in the near future, it sure would be nice to be given money by companies. But there's also more work than I can actually do on my own full time and extra labour would be nice too.

The additional problem is that there a lot of small open source projects that get used by don't really have the numbers that donations would give them enough money to live on, so they can't quit the day job. For those people time is actually much shorter than money.

(Disclaimer: I wrote twodaymanifesto.com)

> Once you've tried property based testing, I think you never really trust things quite the same :)

Oh god, tell me about it. So far I've hit 4 pypy bugs, 3 cpython bugs, two pytz bugs (one caused by a cpython bug), and I've learned far more about the edge cases of the language than I ever wanted to know.

Lets just not talk about the number of bugs I've found in Hypothesis itself in the course of testing bits of the system I was sure worked perfectly.