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

71–80 of 107 posts

Re: Hypothesis, Antithesis, synthesis

#71

Post by sunshowers »

DRMacIver wrote: post #19
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…

> But the problem remains verifying that the tests actually test what they're supposed to. Definitely. It's a lot harder to fake this with PBT than with example-based testing, but you can still write bad property-based tests and agents are pretty good at doing so. I have generally found that agents with property-based tests are much better at not lying to themselves about it than agents with just example-based testin…

A fun recent experience I had with Claude was I asked it to write a model for PBTs against a complex SUT, and it duplicated the SUT algorithm in the model — not helpful! I had to explicitly prompt it to write the model algorithm in a completely different style.

Re: Hypothesis, Antithesis, synthesis

#72

Post by DRMacIver »

sunshowers wrote: post #71
DRMacIver wrote: post #19

Earlier quoted context omitted.

> But the problem remains verifying that the tests actually test what they're supposed to. Definitely. It's a lot harder to fake this with PBT than with example-based testing, but you can still write bad property-based tests and agents are pretty good at doing so. I have generally found that agents with property-based tests are much better at not lying to themselves about it than agents with just example-based testin…

A fun recent experience I had with Claude was I asked it to write a model for PBTs against a complex SUT, and it duplicated the SUT algorithm in the model — not helpful! I had to explicitly prompt it to write the model algorithm in a completely different style.

Ugh, yeah. Duplicating the code under test is a bad habit that Claude has had when writing property-based tests from very early on and has never completely gone away.

Hmm now that you mention it we should add some instructions not to do that in the hegel-skill, though oddly I've not seen it doing it so far.

Re: Hypothesis, Antithesis, synthesis

#73

Post by DRMacIver »

nz wrote: post #68
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 a…

You're very welcome! I'm glad it's been useful for you.

Re: Hypothesis, Antithesis, synthesis

#74

Post by keeganpoppen »

love the hegel reference. i know hypothesis is awesome, and so im certain this is as well. this is no real complaint about the post, because it is a personal skill issue, but for someone who is more of a PL nerd than… most people on earth… i find Ruat code to be some of the hardest to actually parse in any meaningful way. even to get a sense of how the property defs were being set up, i kinda just took it at face value that it is cool… i guess it really comes down to personally not having much interest in rust compared to most newfangled languages out there. like i said, skipl issue, not a conplaint. wish you all the best, and lots of success!

Re: Hypothesis, Antithesis, synthesis

#75

Post by lwhsiao »

DRMacIver wrote: post #39
lwhsiao wrote: post #28

DRMacIver, can you comment on how this fits into the existing property-based testing ecosystems for various languages? E.g., if I use proptest in Rust, why would/should I switch to Hegel?

The short answer to how it fits into existing ecosystems is... in competition I suppose. We've got a lot of respect for the people working on these libraries, but we think the Hypothesis-based approach is better than the various approaches people have adopted. I don't love that the natural languages for us to start with are ones where there are already pretty good property-based testing libraries whose toes we're ste…

This is helpful, thanks!

Re: Hypothesis, Antithesis, synthesis

#76

Post by tybug »

DRMacIver wrote: post #70
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.

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.

`from_type` just supports a bunch more things than rust ever can due to the flexibility of python's type system. `from_type(object)` is amazing, for example, and not something we can write in rust.

Re: Hypothesis, Antithesis, synthesis

#77

Post by ruuda »

Property-based testing is nice, but making it coverage-driven is a game changer. It will explore code paths that naive random inputs will not trigger in a thousand years. In Rust this works very well with libFuzzer and the Arbitrary crate to derive the generators.

Re: Hypothesis, Antithesis, synthesis

#78

Post by tybug »

DRMacIver wrote: post #17
anentropic wrote: post #10

Earlier quoted context omitted.

TBH reading the first few words of that section I was definitely expecting it to continue "so we used Claude to rewrite Hypothesis in Rust..." so that was quite a surprise!

It's on the agenda! We definitely want to rewrite the Hegel core server in rust, but not as much as we wanted to get it working well first. My personal hope is that we can port most of the Hypothesis test suite to hegel-rust, then point Claude at all the relevant code and tell it to write us a hegel-core in rust with that as its test harness. Liam thinks this isn't going to work, I think it's like... 90% likely to ge…

To put it on the record: my position is current models can't get us there, and neither can the next iteration of models, but in two model iterations this will be worth doing. There's a lot of fiddly details in Hypothesis that are critical to get right. You can get a plausible 80% port with agents today but find they've structured it in a way to make it impossible to get to 100%.

Re: Hypothesis, Antithesis, synthesis

#79

Post by wwilson »

ruuda wrote: post #77

Property-based testing is nice, but making it coverage-driven is a game changer. It will explore code paths that naive random inputs will not trigger in a thousand years. In Rust this works very well with libFuzzer and the Arbitrary crate to derive the generators.

[Disclaimer: Started Antithesis]

If you run your Hegel tests in Antithesis, you get this for free (along with various sorts of “non-local” assertions, perfect reproducibility even for concurrent or distributed code, etc.).

But yeah, not hard to hack together basic coverage guidance outside Antithesis. That works well for large classes of programs, just not a majority of them.

Re: Hypothesis, Antithesis, synthesis

#80

Post by Groxx »

js8 wrote: post #57
Groxx wrote: post #43

Earlier quoted context omitted.

And how do you know if it has proven the property you want, instead of something that's just complicated looking but evaluates to true?

The AI would build a proof of correctness, which would be then verified in a proof checker (not AI).

And how do you prove that the proof of correctness is not just a proof that 1=1? LLMs "cheating" on things is rather common.
Post reply on HN