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

81–90 of 107 posts

Re: Hypothesis, Antithesis, synthesis

#81

Post by skybrian »

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…

I'm not sure either of us really knows how Curry-Howard works, but my understanding is that it's a compile-time type system thing. In certain proof languages, a function that returns an int proves that an int exists (type is inhabited). And that's just not very interesting - you need more sophisticated types than we commonly use. Also, it only works for total functions, so it's not true in most ordinary programming languages.

So I'm skeptical that the code we write in ordinary programming languages proves anything interesting. Why do you think that?

Re: Hypothesis, Antithesis, synthesis

#82

Post by epage »

LoganDark wrote: post #63

Using Python from other languages is terrible. I love this kind of testing but this implementation is not for me. I was so excited before learning it depends on Python.

Yeah, having `cargo test` require another binary like `uv` is not idiomatic. 99% of the time, I should be able to walk up to a Rust project and run `cargo test` and it should just work.

Re: Hypothesis, Antithesis, synthesis

#83

Post by skybrian »

chriswarbo wrote: post #61
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 discar…

It's not like how it's done in that paper, but oddly enough I did end up implementing some conversions in both directions, from an array of choices to a JavaScript object and back again.

https://jsr.io/@skybrian/repeat-test/doc/core/~/Domain

Re: Hypothesis, Antithesis, synthesis

#85

Post by beedeebeedee »

AndrewKemendo wrote: post #38
sigbottle wrote: post #27

Earlier quoted context omitted.

I mean I don't know about Hegel, but Kant certainly dipped into mathematics. One of the reasons why he even wrote CPR was to unify in his mind, the rationalists (had Leibniz) versus the empiricists (had Newton). 20th century analytic philosophy was heavily informed by Kantian distinctions (Logical Positivism uses very similar terminology, and Carnap himself was a Neo-Kantian originally, though funnily enough Heidegge…

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…

> Hegel is irrelevant in the age of measurement

That’s bs. Even just the preface to Phenomenology of Spirit is chock full of ideas that folks would be better off if they contemplated. Hegel can be considered a visual thinker (or visionary) whose ideas don’t need “measurement”. If folks understand his thoughts on the master-slave dialectic, for example, they would have an idea as to why we have such incompetent leaders like trump. His thought suffers from the same problem of any thinker who tried to be systematic, but it is still worth being inspired by.

Re: Hypothesis, Antithesis, synthesis

#86

Post by ahf8Aithaex7Nai »

To all you amateur Hegel enthusiasts out there: there is no synthesis in Hegel.

Otherwise: Congratulations on the QuickCheck-style testing in Rust. At work, I’m always surprised that property-based testing is so little known and so rarely used outside of functional programming.

Re: Hypothesis, Antithesis, synthesis

#87

Post by DiscourseFan »

ahf8Aithaex7Nai wrote: post #86

To all you amateur Hegel enthusiasts out there: there is no synthesis in Hegel. Otherwise: Congratulations on the QuickCheck-style testing in Rust. At work, I’m always surprised that property-based testing is so little known and so rarely used outside of functional programming.

“Synthesis” is the purposiveness in the force of the Concept.

Re: Hypothesis, Antithesis, synthesis

#88

Post by dr_dshiv »

ahf8Aithaex7Nai wrote: post #86

To all you amateur Hegel enthusiasts out there: there is no synthesis in Hegel. Otherwise: Congratulations on the QuickCheck-style testing in Rust. At work, I’m always surprised that property-based testing is so little known and so rarely used outside of functional programming.

yeah where did that come from? It's like attributing the cartesian coordinate plane to Descartes -- when actually it was a textbook author who came up with the modern one...

Re: Hypothesis, Antithesis, synthesis

#90

Post by mpalmer »

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…

What about "this is actually harming us right now"?
Post reply on HN