Clojurians Log v2

Different testing/verification techniques have different reach. If you can prove a property inside of a system then consistency is guaranteed. Generative tests don't do that. Concretely, I have used generative testing extensively against the https://github.com/replikativ/persistent-sorted-set that many of the replikativ libraries now use to spot errors, but one that was in there already from the beginning only showed up by chance in one run and I am still not sure my fix fully covered it. If you compare this to the verification of the RBTree in the README https://github.com/replikativ/ansatz, then there you can be sure the tree is always balanced for instance. Now, your assessment is right that often proving is too much effort and you have to make idealistic assumptions, e.g. have no caching, IO, side effects, use no standard Clojure functions etc. But even then there are cases where I would say it is actually instructive to try to prove a property you care about, let's say consistency of a statistical estimator, even if the proof does not fully apply to your code. It will help you to improve your implementation and understanding. And importantly most frontier LLMs are now very good at using Lean and mathlib and you can let them chew a bit on something you care about while learning from it. Does this make sense?

Would you say then you would keep testing?

I would say that this is also the reason to gradually type your programs. If you know the types and the type system captures consistency you care about, then it is worth it.

For sure, I am not saying you should prioritize Ansatz. But you can try to apply it to formal bits of your code that are mathematically or formally well specified. Such as data structures, algorithms, stats estimators, etc.

This is why I put this here for instance https://github.com/replikativ/ansatz/blob/main/examples/gradient_descent.clj, it is something you would prove in a grad class on optimization/machine learning (we had this here), and you can prove it directly on your running code.

If anything it is a great learning opportunity to bridge the gap from programming to constructive maths, which can make it a lot easier to learn it without going to a university.

I think Clojure should have a gradual/optional type system like typedclojure and libraries should provide optional type annotations. It is weird that Python and JavaScript have been able to do this, but somehow Clojure decided it is not worth it. Python got so much nicer to work with since it has type annotations.

In general you want to make use of the fact that you have access to non-opinionated prodigy programmers and let them apply the sharpest tools to a problem, even if you don't understand it yet or it is a speculative experiment. The cost of verification has dropped by many orders of magnitude now and Ansatz itself makes it much easier to just pull it in in a REPL and play around.

When I ask Claude how this can help me it's only to reduce probability from property based tests and use mathematical proof as opposed to a brute force verification process. Lines of code difference in an existing codebase would not change that much. What use cases exist for this outside of that?