tybug

We plan to rewrite hypothesis in rust and expose an FFI through that! This is a medium term plan (months, not weeks or years), but we're acutely aware that relying on a python component is not a long-term solution.

Yes! I just wrote up documentation for the protocol earlier this week: https://hegel.dev/reference/protocol.

In reality, we hope to provide more guidance than this to people who want to write their own language frontend. This protocol reference doesn't talk about the realities of [hegel-core](https://github.com/hegeldev/hegel-core) and how to invoke it, for example.

We intend to write a "How to write your own Hegel library" how-to guide. You can subscribe to this issue to get notified when we write that: https://github.com/hegeldev/website/issues/3.

If you're eager, pointing your favorite LLM at https://hegel.dev/reference/protocol + https://github.com/hegeldev/hegel-rust and asking it to write you one for your language of choice should be enough to get you started!

I didn't expect to see Hegel when opening up HN today! Feel free to ask any questions about it. We released hegel-go earlier this week, and plan to release hegel-cpp sometime next week, so look forward to that :)

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

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

Yep, `#[derive(DefaultGenerator)]` and `generators::default<T>()` 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.

I actually think there's another angle here where PBT helps, which wasn't explored in the blog post.

That angle is legibility. How do you know your AI-written slop software is doing the right thing? One would normally read all the code. Bad news: that's not much less labor intensive as not using AI at all.

But, if one has comprehensive property-based tests, they can instead read only the property-based tests to convince themselves the software is doing the right thing.

By analogy: one doesn't need to see the machine-checked proof to know the claim is correct. One only needs to check the theorem statement is saying the right thing.

As possibly the one community on earth where it's actually better to post the code than the blog post: TL;DR this is a universal property-based testing protocol (https://github.com/hegeldev/hegel-core) and family of libraries (https://github.com/hegeldev/hegel-rust, more to come later).

I've talked with lots of people in the PBT world who have always seen something like this as the end goal of the PBT ecosystem. It seemed like a thing that would happen eventually, someone just had to do it. I'm super excited to actually be doing it and bringing great PBT to every and any language.

It doesn't hurt that this is coming right as great PBT in every language is suddenly a lot more important thanks to AI code!

Appreciate the thoughts <3. I do think there might be stronger examples we could choose. Possibly json encode/decode..

(Hypothesis maintainer here) If you have recommendations for a better example on the front page, I'd love to hear them! (I mean this entirely genuinely and non-sarcastically; I agree sorting can give misleading ideas, but it is also concise and well understood by every reader).

(Hypothesis maintainer here)

Yup, a standard test suite just doesn't run for long enough for coverage guidance to be worthwhile by default.

That said, coverage-guided fuzzing can be a really valuable and effective form of testing (see eg https://hypofuzz.com/).

Nice! "testing your test code" is particularly important when dealing with PBT distributions, especially when your generator gets more complicated.

Tyche [0] is another cool tool for addressing the same problem, visualizing the PBT distribution but not making assertions about it.

[0] https://github.com/tyche-pbt/tyche-extension

The Hypothesis explain phase [1][2] does this!

  fails_on_empty_third_arg(
      a = "",  # or any other generated value
      b = "",  # or any other generated value
      c = "",  
      d = "",  # or any other generated value
  )

[1] https://hypothesis.readthedocs.io/en/latest/reference/api.ht...

[2] https://github.com/HypothesisWorks/hypothesis/pull/3555

That kind of behavior can happen at the threshold of Hypothesis' internal limit on entropy - though if you're not hitting HealthCheck.data_too_large then this seems unlikely.

Let me know if you have a reproducer, I'd be curious to take a look.

(not OP but I would be surprised if the answer wasn't) yes, because you're changing the order in which the random draws are interpreted. But this isn't a problem in practice because you generally aren't changing the generator in the middle of debugging a failure.

You're right, I misstated this - but I don't think this is fatal. The other sibling commenters pointed out the real issue with my thinking.

The argument goes the same even though I misspoke here. If the machine {halts, runs forever} then ZFC is consistent. But this is a contradiction; so ZFC must be inconsistent. Tada, I have an inconsistency proof!

That was the implied next step which made me think my logic was clearly incorrect (which, it was).

I suppose I did!

I was having a hard time reconciling this with the intuition that BB(n) is in principle "computable" (colloquially speaking) for any n - my thinking went that if I want to compute BB(n), I can enumerate turing machines and run them until they halt, since infinitely looping machines are excluded from BB(n). But of course I have now reduced this to the halting problem! How do you know when you're "done" for that n? You don't.

Thanks to you and sibling commenters.

I'm hoping someone can enlighten me here. My understanding is that there is a turing machine of 748 states [0], which halts iff ZFC is inconsistent (Thm 1). But this machine is a "physical" object, in the sense that we can materialize it on a computer and run it. Though we don't have the computing power for this currently, there is nothing in principle stopping us from running this machine for BB(748) steps: if it halts, we have proven by Thm 1 that ZFC is inconsistent. If not, we have similarly proven that ZFC is consistent.

I want to stress that this is key to my confusion. This is not just some abstract result; this is a computation that we can perform and draw a real value from.

Of course, I'll now fall back on godel's second incompleteness theorem and say that one cannot prove, inside ZFC, that ZFC is consistent. But if the above turing machine halts, then we proved ZFC is consistent - a contradiction!

Where is the mistake here? My current guess is there is a technical detail in the proof of Thm 1 which uses a stronger metatheory than ZFC to show that the 758-state turing machine halts iff ZFC is inconsistent. This is not a contradiction, because yes, we can run the turing machine for BB(748) steps, but that will only show that ZFC+ proves ZFC is consistent, which is already well known - ZFC + there exists an inaccessible cardinal does the job.

However, I haven't looked at the paper in detail to know whether this is the case. Does anybody who has thought deeply about this problem have insight to offer?

[0] https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-unde...

No disagreement here. But I hold that this is an especially confusing way of describing independent statements, especially in this paper, which certainly was written by a logician.

I take particular issue with the phrasing because it confused me for years in highschool and throughout undergraduate. How could something be true and not provable? It took me until a model theory course to realize that it cannot, and most pop descriptions of the incompleteness theorem are - dare I say it - wrong. Though I'm sure you would argue it's not wrong, merely an informal description.

I would, however, expect a bachelor's thesis not to stray into such confusing territory.

A common misconception in the first paragraph:

> However, Godel shattered these aspirations in 1931 by proving the existence of true but unprovable mathematical formulas.

Godel sentences are unprovable, but they are not "true". They are independent, i.e. true in some models and false in others. The godel sentence happens to be true in the standard model - some people take liberties with this and extend to calling it true, but that's not accurate, or at the very least misleading.

Formal systems need not be consistent; if a formal system assumes both P and ~P as axioms, you can derive S and ~S (for any S) by explosion.

I would argue "reasoning about programs" formally means "can prove P Q R ..." (with appropriate choices for P Q R) and doesn't implicitly carry an assumption of consistency. But, fair enough.

> But the same reasoning can be applied to any formal system F, with fairly minimal assumptions:

Strictly speaking, F has to be satisfiable/consistent as well. {P, ~P} is a trivially recursively enumerable, complete theory which contains Q.

I realize this quote isn't meant to be taken literally, and it's a nice one-liner encapsulation of metaclasses, but it always bothered me. The people who "actually need metaclasses" were, at some point, learning about metaclasses for the first time and were "wondering whether they need them".

This quote ignores the middle ground of users who have a valid use case, but don't yet understand metaclasses. Not great advice for people who are trying to learn metaclasses.

The most salient example I can think of is tracking all subclasses of a class. This is how django tracks `Model` subclasses to create a table for each model, for instance. I wrote a blog post on this topic: https://tybug.github.io/2021/11/06/tracking-all-subclasses-o...

I've also used metaclasses in the past to apply a decorator to certain methods of all subclasses, without needing to specify that decorator in the subclass declaration itself.