Hacker News Reader

Comment by kccqzy | Hacker News Reader

It’s a standard way to do pre and post conditions. Clojure pre and post conditions also behave this way. If you force these conditions into compile-time checks, well, then you are introducing a second type system with refinement types into the language. And type checking would take a long time. Imagine someone writes a precondition for a function where its integer argument x needs to satisfy collatz(x)==1; do you now expect the compiler to prove the collatz conjecture or verify it for all 64-bit integers every compilation?

My experience using pre and post conditions in Clojure makes me really like them. They are a small but meaningful improvement over plain old assertions. And yes being able to turn them off is a feature not a bug. Don’t expect them to be like LiquidHaskell.

View on HN

SPARK (Ada) has compile time pre and post conditions, and it works well. If you declare the post-condition Collatz (n) = 1, the compiler can't help you, and compilation will fail. If you've got a difficult condition, you're going to have to help the theorem prover, often by introducing "ghost" functions, or by simply softening the condition. In the latter case, you can't prove total correctness, but you can often still prove things like absence of run-time errors.

Off-topic, but collatz(x) == 1 for all positive 64-bit integers (actually, this has been verified up to 2^71: https://link.springer.com/article/10.1007/s11227-025-07337-0). I recently made this tool if anyone wants to try it with 1,000-digit integers or ranges: https://www.proofatlas.ai/explore/collatz/.

Just curious, but what's the definition of collatz(long) look like?

https://en.wikipedia.org/wiki/Collatz_conjecture

I meant the C++ definition of collatz that would verify the precondition.

I haven't tried it and am afk rn but I'd imagine you just define a constexpr function that implements collatz and use that in your contract.

(Edit: if the input is constexpr itself) Its also quire easy to think about specializing a few templates and doing it that way. If you look up an example of the fib sequence in c++ templates you'll get the general idea.

I feel like I'd have something to learn from seeing the code.

Won't you just run into a constexpr evaluation depth error with a suggestion to set -fconstexpr-depth? I don't see how this is the gotcha it's made out to be.

I'd exepct something like that to happen. Worth reiterating that the whole scenario is for a hypothetical different implementation of contract that would execute comptime, as noted in the parent thread.

If you wanted a c++26 preconditon for collatz tho, here it is. ```cpp bool collatz(unsigned long long n) { while (n != 1) n = n % 2 ? 3 * n + 1 : n / 2; return true; }

void f(unsigned long long n) pre(collatz(n)); ``` That's basically what you'd write if you were doing it with asserts, as the linked article states, just now you add it to the declaration.

You may have to internally use bignums since collatz orbits can become very large before shrinking.

That's a good point. I wonder how difficult comptime bignum would be in comptime. Seems like there's no proven bounds I could find either

> If you wanted a c++26 preconditon for collatz tho, here it is.

  cpp bool collatz(unsigned long long n)
  {
    while (n != 1)
      n = n % 2 ? 3 * n + 1 : n / 2;
    return true;
  }

You’ll need to add code to detect cycles other than 1, 4, 2, 1, 4, 2,… to that. That can be done in constant space (https://en.wikipedia.org/wiki/Cycle_detection#Floyd’s_tortoi...)

Ideally, you also need a way to detect runs towards infinity. That is harder.

Otherwise, an optimising compiler can use the forward progress guarantee and optimize that to:

  cpp bool collatz(unsigned long long n)
  {
    return true;
  }

and then completely remove the precondition.

I think I saw years ago that clang replaced a collatz impl with true. Why is it that the "forward progress garuntee" would let it do that?

You may think about this blog post from John Regehr about Fermat's Last Theorem: https://blog.regehr.org/archives/140

Thanks! Great read, and makes good sense.

For future readers his sequel post explains the specific cause.

https://blog.regehr.org/archives/161

Reply on news.ycombinator.com