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!

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.

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!

Comments URL: https://news.ycombinator.com/item?id=46978534

Points: 2

# Comments: 0

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

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

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

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

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

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

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.