alt Hacker NewsIt’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.
Replies
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.
Just curious, but what's the definition of collatz(long) look like?
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/.