Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Hypothesis, Antithesis, synthesis

antithesis.com

Post reply on HN
Print view View original

61–70 of 107 posts

Re: Hypothesis, Antithesis, synthesis

#61

Post by chriswarbo »

skybrian wrote: post #34

It isn't used by anyone besides me, but I wrote a property-testing library for Deno [1] that has a form of "sometimes" assertions (inspired by Antithesis) and uses "internal shrinking" (inspired by Hypothesis). But it's still a "blind" fuzzer and it would be nice to write one that gets feedback from code coverage somehow. Instead, you have to run code coverage yourself and figure out how to change test data generatio…

> But it's still a "blind" fuzzer and it would be nice to write one that gets feedback from code coverage somehow

There have been simplistic attempts at this, e.g. instead of performing 100 tests, just keep going as long as coverage increases.

The Choice Gradient Sampling algorithm from https://arxiv.org/pdf/2203.00652 feels like a nice way to steer generators in a more nuanced way. That paper uses it to avoid discards when rejection-sampling; but I have a feeling it could be repurposed to "reward" based on new coverage instead/as-well.

Re: Hypothesis, Antithesis, synthesis

#62

Post by pmbauer »

zoogeny wrote: post #54
pron wrote: post #8

> property-based testing is going to be a huge part of how we make AI-agent-based software development not go terribly. There's no doubt, I think, testing will remain important and possibly become more important with more AI use, and so better testing is helpful, PBT included. But the problem remains verifying that the tests actually test what they're supposed to. Mutation tests can allow agents to get good coverage…

> t took humans years to write the tests by hand, and the agents still failed to converge. I think there is some hazard in assuming that what agents fail at today they will continue to fail on in the future. What I mean is, if we take the optimistic view of agents continuing to improve on the trajectory they have started at for one or two years, then it is worth while considering what tools and infrastructure we will…

> I think there is some hazard in assuming that what agents fail at today they will continue to fail on in the future.

I think there is some hazard in assuming a seemingly exponential curve has no asymptotes, otherwise known as faith.

Re: Hypothesis, Antithesis, synthesis

#64

Post by zoogeny »

pmbauer wrote: post #62
zoogeny wrote: post #54

Earlier quoted context omitted.

> t took humans years to write the tests by hand, and the agents still failed to converge. I think there is some hazard in assuming that what agents fail at today they will continue to fail on in the future. What I mean is, if we take the optimistic view of agents continuing to improve on the trajectory they have started at for one or two years, then it is worth while considering what tools and infrastructure we will…

> I think there is some hazard in assuming that what agents fail at today they will continue to fail on in the future. I think there is some hazard in assuming a seemingly exponential curve has no asymptotes, otherwise known as faith.

That is what the market is for!

I'm just pointing out "we don't need this right now" isn't necessarily an argument against "we don't need this".

There is a saying that isn't perfect but may apply: better to have it and not need it then to need it and not have it.

Here is another way of looking at it. Let's say agents don't meet the hyped up expectations and we build all of this robust tooling for nothing. So we have all of this work towards creating autonomous testing systems but we don't have the autonomous agents. That still seems like a decent outcome.

When we plan around optimistic views of the future, we tend to build generally useful things.

Re: Hypothesis, Antithesis, synthesis

#65

Post by DRMacIver »

sunshowers wrote: post #58
tybug wrote: post #55

Earlier quoted context omitted.

Yep, `#[derive(DefaultGenerator)]` and `generators::default ()` are the right tools here. This is one of the areas we've dogfooded the least, so we'd definitely be happy to get feedback on any sharp corners here! I think `from_type` is one of Hypothesis's most powerful and ergonomic strategies, and that while we probably can't get quite to that level in rust, we can still get something that's pretty great.

Thank you! I have some particularly annoying proptest-based tests that I'll try porting over to Hegel soon. (Thanks for writing the Claude skill to do this.)

Please let us know how it goes!

As Liam says, the derive generator is not very well dogfooded at present. The claude skill is a bit better, but we've only been through a few iterations of using it and getting Claude to improve it, and porting from proptest is one of the less well tested areas (because we don't use proptest much ourselves).

I expect all of this works, but I'd like to know ways that it works less well than it could. Or, you know, to bask in the glow of praise of it working perfectly if that turns out to be an option.

Re: Hypothesis, Antithesis, synthesis

#66

Post by pfdietz »

DRMacIver wrote: post #24
Chinjut wrote: post #22

Earlier quoted context omitted.

You mention in the post that there are design differences between Hegel/Hypothesis and QuickCheck, partly due to attitude differences between Python/non-Haskell programmers and Haskell programmers. As someone coming from the Haskell world (though by no means considering Haskell a perfect language), could you expand on what kinds of differences these are?

So I think a short list of big API differences are something like: * Hypothesis/Hegel are very much focused on using test assertions rather than a single property that can be true or false. This naturally drives a style that is much more like "normal" testing, but also has the advantage that you can distinguish between different types of failing test. We don't go too hard on this, but both Hegel and Hypothesis will r…

I'd love to see all this integrated with mutation testing, the thing being looked for being that the test input kills the mutant.

Re: Hypothesis, Antithesis, synthesis

#67

Post by chriswarbo »

js8 wrote: post #56
skybrian wrote: post #44

Earlier quoted context omitted.

Proofs are a form of static analysis. Static analysis can find interesting bugs, but how a system behaves isn't purely a property of source code. It won't tell you whether the code will run acceptably in a given environment. For example, if memory use isn't modelled, it won't tell you how big the input can be before the system runs out of memory. Similarly, if your database isn't modelled then you need to test with a…

> Databases and web browsers are too complicated to build a full-fidelity mathematical model for. I disagree - thanks to Curry-Howard isomorphism, the full-fidelity mathematical model of a database or web browser are their binaries themselves. We could have compilers provide theorems (with proof) of correctness of the translation from source to machine code, and library functions could provide useful theorems about t…

> thanks to Curry-Howard isomorphism, the full-fidelity mathematical model of a database or web browser are their binaries themselves.

Maybe I'm misunderstanding you, but Curry-Howard is a mapping between mathematical jargon and programming jargon, where e.g. "this is a proof of that proposition using foo logic" maps to "this program has that type in programming language foo".

I don't see how that makes "binaries" a "full-fidelity mathematical model": compilation is (according to Curry-Howard) translating a proof from one system of logic to another. For a binary, the resulting system of logic is machine code, which is an absolutely terrible logic: it has essentially one type (the machine word), which makes every proposition trivial; according to Curry-Howard, your database binary is proof of the proposition corresponding to its type; since the type of every binary is just "some machine words", the proposition that your database binary is a "full-fledged mathematical model" of is essentially just "there exists a machine word". Not very useful; we could optimise it down to "0", which is also a proof that there exists a machine word.

If we assume that you want to prove something non-trivial, then the first thing you would need to do is abstract away from the trivial logic of machine code semantics, by inferring some specific structures and patterns from that binary, then developing some useful semantics which captures those patterns and structures. Then you can start to develop non-trivial logic on those semantics, which will let you state worthwhile propositions. If we apply the Curry-Howard lens to that process, it corresponds to... decompilation into a higher-level language!

tl;dr Curry-Howard tells us that binaries are literally the worst possible representation we could hope for.

Re: Hypothesis, Antithesis, synthesis

#68

Post by nz »

DRMacIver wrote: post #2

Post author here btw, happy to take questions, whether they're about Hegel in particular, property-based testing in general, or some variant on "WTF do you mean you wrote rust bindings to a python library?"

Not really a question. Just wanted to express my gratitude for Hypothesis. I use it regularly. A few years back, I had to build a semi-formally-verified fund and account management service, and used the state-based-testing of Hypothesis to validate its correctness. Cannot express how invaluable this little framework has been.

A little while after that, I spoke to someone in the pharma-adjacent-space who was looking at Antithesis to validate their product. At the time, Antithesis (the company) told him that it was a bad fit. I suggested something akin to my previous approach (which did not include antithesis). No clue what they ended up doing, but it is nice to see that Hypothesis and Antithesis have finally joined forces.

Re: Hypothesis, Antithesis, synthesis

#69

Post by FridgeSeal »

zoogeny wrote: post #64
pmbauer wrote: post #62

Earlier quoted context omitted.

> I think there is some hazard in assuming that what agents fail at today they will continue to fail on in the future. I think there is some hazard in assuming a seemingly exponential curve has no asymptotes, otherwise known as faith.

That is what the market is for! I'm just pointing out "we don't need this right now" isn't necessarily an argument against "we don't need this". There is a saying that isn't perfect but may apply: better to have it and not need it then to need it and not have it. Here is another way of looking at it. Let's say agents don't meet the hyped up expectations and we build all of this robust tooling for nothing. So we have…

The market stopped being remotely useful measurement of…anything quite a while ago.

Re: Hypothesis, Antithesis, synthesis

#70

Post by DRMacIver »

tybug wrote: post #55
sunshowers wrote: post #51

Hi David, congratulations on the release! I'm excited to play around with Hypothesis's bitstream-based shrinking. As you're aware, prop_flat_map is a pain to deal with, and I'd love to replace some of my proptest-based tests with Hegel. I spent a little time looking at Hegel last week and it wasn't quite clear to me how I'd go about having something like a canonical generator for a type (similar to proptest's Arbitra…

Yep, `#[derive(DefaultGenerator)]` and `generators::default ()` are the right tools here. This is one of the areas we've dogfooded the least, so we'd definitely be happy to get feedback on any sharp corners here! I think `from_type` is one of Hypothesis's most powerful and ergonomic strategies, and that while we probably can't get quite to that level in rust, we can still get something that's pretty great.

What do you think we're currently missing that Python's `from_type` has? I actually think the auto-deriving stuff we currently have in Rust is as good or better than from_type (e.g. it gets you the builder methods, has support for enums), but I've never been a heavy from_type user.
Post reply on HN