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

51–60 of 107 posts

Re: Hypothesis, Antithesis, synthesis

#51

Post by sunshowers »

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 Arbitrary). I've found that to be very helpful while generating large structures to test something like serialization roundtripping against — in particular, the test-strategy library has derive macros that work very well for business logic types with, say, 10-15 enum variants each of which may have 0-10 subfields. I'm curious if that is supported today, or if you have plans to support this kind of composition in the future.

edit: oh I completely missed the macro to derive DefaultGenerator! Whoops

Re: Hypothesis, Antithesis, synthesis

#52

Post by viccis »

sigbottle wrote: post #36
viccis wrote: post #30

Earlier quoted context omitted.

>other techniques include Kant's Transcendental Deduction or Descartes's pure doubt This is not quite accurate. Kant says very explicitly in the (rarely studied) Transcendental Doctrine of Method (Ch 1 Section 4, A789/B817) that this kind of proof method (he calls it "apagogic") is unsuitable to transcendental proofs. You might be thinking of the much more well studied Antinomies of Pure Reason, in which he uses this…

Sorry I meant "proof method" as more like "this was this guy's angle of attack", not that they would've thought each others angles were valid at all or that they're commensurable with say, 20th century formal proof logic (or Aristotelian logic for example). Descartes and Leibniz were squarely the rationalists that Kant wanted to abolish, and Hegel rejected Kants distinction between noumena and phenomena entirely, so…

>I guess I have not thought critically why we couldn't use a Transcendental argument to support Descartes.

The previous section within the Transcendental Dialectic that focuses on the nature of the soul goes into a refutation of Descartes' statement. Kant basically finds "I think therefore I am" to be a tautology that only works by equivocating the "I" in each clause. "I think" pretends that the "I" there is an object in the world which it then compares to the "I am" which is an object in the world. Kant argues that "I think" does not actually demonstrate an "I" that is an object but rather a redundant qualification of thinking.

I am being a bit imprecise, so here is SEP's summary:

>For in each case, Kant thinks that a feature of self-consciousness (the essentially subjectival, unitary and identical nature of the “I” of apperception) gets transmuted into a metaphysics of a self (as an object) that is ostensibly “known” through reason alone to be substantial, simple, identical, etc. This slide from the “I” of apperception to the constitution of an object (the soul) has received considerable attention in the secondary literature, and has fueled a great deal of attention to the Kantian theory of mind and mental activity.

>The claim that the ‘I’ of apperception yields no object of knowledge (for it is not itself an object, but only the “vehicle” for any representation of objectivity as such) is fundamental to Kant’s critique of rational psychology.

[1] https://plato.stanford.edu/entries/kant-metaphysics/#SouRatP...

Re: Hypothesis, Antithesis, synthesis

#53

Post by jmalicki »

sigbottle wrote: post #45
AndrewKemendo wrote: post #38

Earlier quoted context omitted.

My claim is that genuinely all of those previous analytical forms are absolutely useless if you have the capacity to utilize a more mathematical framework The problem is, those more mathematically challenging frameworks are inaccessible to the majority of the people so they don’t actually take off because there’s no mechanism to translate more rigor in social studies and social sciences in large part because humans r…

Oh interesting. I've basically quotiented out all social science all my life and stuck strictly to STEM, so my stack is, a lot of analytic + philosophy of science. A lot of pure math and CS (all across the stack), and recently physics because of job. I try not to comment on social issues (though Continental vibes generally seem righter to me the more I study it) But I've never thought critically (in a long time) abou…

Microeconometrics tends to be quite rigorous and easy to validate.

They won't hold up to physics levels of rigor, of course - probably a bit more at the medical studies level of rigor.

David Card, Gary Becker, McFadden, etc.

Rigor is also... there's something about letting perfect be the enemy of the good.

If noone will apply math unless you can 100% reliably reproduce controlled experiments in a lab, the only thing left is people just talking about dialectics.

The challenge is how to get as much rigor as possible.

For instance, David Card saw New Jersey increase minimum wage. You generally can't truly conduct large-scale controlled social experiments, but he saw this as interesting.

He looked at the NJ/PA area around Philadelphia as a somewhat unified labor market, but half of it just had its minimum wage increased - which he looked at to study as a "natural" experiment, with PA as the control group and NJ as the experimental group, to investigate what happened to the labor market when the minimum wage increased. Having a major metro area split down the middle allowed for a lot of other concerns to be factored out, since the only difference was what side of the river you happened to be on.

He had lots of other studies looking at things like that, trying to find ways to get controlled-experiment like behavior where one can't necessarily do a true controlled experiment, but trying to get as close as possible, to be as rigorous as is possible.

Is that as ideal as a laboratory experiment? Hell no. But it's way closer than just arguing dialectics.

Re: Hypothesis, Antithesis, synthesis

#54

Post by zoogeny »

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 need for them. Companies that start to build that now for the future they assume is coming are going to be better positioned than people who wake up to a new reality in two years.

Re: Hypothesis, Antithesis, synthesis

#55

Post by tybug »

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.

Re: Hypothesis, Antithesis, synthesis

#56

Post by js8 »

skybrian wrote: post #44
js8 wrote: post #32

Earlier quoted context omitted.

> 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. Given Curry-Howard isomorphism, couldn't we ask AI to directly prove the property of the binary executable under the assumption of the HW model, instead of running PBTs? By no means I want to dismiss PBTs - but it seems that this could be both faster and more…

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 the resource use.

Then, if the AI can reason about the behavior of the source code, it can also build the required proof of correctness along with it.

Re: Hypothesis, Antithesis, synthesis

#57

Post by js8 »

Groxx wrote: post #43
js8 wrote: post #32

Earlier quoted context omitted.

> 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. Given Curry-Howard isomorphism, couldn't we ask AI to directly prove the property of the binary executable under the assumption of the HW model, instead of running PBTs? By no means I want to dismiss PBTs - but it seems that this could be both faster and more…

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).

Re: Hypothesis, Antithesis, synthesis

#58

Post by sunshowers »

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.

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.)

Re: Hypothesis, Antithesis, synthesis

#59

Post by groby_b »

js8 wrote: post #32
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…

> 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. Given Curry-Howard isomorphism, couldn't we ask AI to directly prove the property of the binary executable under the assumption of the HW model, instead of running PBTs? By no means I want to dismiss PBTs - but it seems that this could be both faster and more…

> Given Curry-Howard isomorphism, couldn't we ask AI to directly prove the property of the binary executable under the assumption of the HW model, instead of running PBTs?

Yes, in principle. Given unlimited time and a plentiful supply of unicorns.

Otherwise, no. It is well beyond the state of the art in formal proofs for the general case, and it doesn't become possible just because we "ask AI".

And unless you provide a formal specification of the entire set of behavior, it's still not much better than PBT -- the program is still free to do whatever the heck it wants that doesn't violate the properties formally specified.

Post reply on HN