[ebiederm]

I appreciate that I am not the only one seeing the connection between property based testing and proofs.

I will quibble a little with their characterization of proofs as being more computationally impractical.

Proof verification is cheap. On a good day it is as cheap as type checking. Type checking being a kind of proof verification. That said writing proofs can be tricky.

I am still figuring out what writing proofs requires. Anything beyond what your type system can express currently requires a different set of tools (Rocq, Lean, etc) than writing asserts and ordinary programs. Plus writing proofs tends to have lots of mundane details that can be tedious to write.

So while I agree proofs seem impractical. I won't agree the reason is computational cost.

[jasongross]

There is a tradeoff between the compute required to generate a proof and the compute required to check it. Fully generic methods such as SMT solvers require compute exponential in the number of variables in scope and lines of code in a single function. Breaking the exponential requires (and is perhaps equivalent to) understanding the code in sufficient detail (cf https://arxiv.org/abs/2406.11779). In practice, the computational cost of semi-automated proof generation is a significant bottleneck, cf https://dspace.mit.edu/handle/1721.1/130763?show=full and https://jasongross.github.io/papers/2022-superlinear-slownes... .

[UncleEntity]

I've been working on this thing where the proofs (using the esbmc library) check the safety properties and the unit tests check the correctness so the state space doesn't explode and it takes a year to run the verification. Been working out pretty well so far (aside from spending more time tracking down esbmc bugs than working on my own code) and found some real issues, mostly integer overflow errors but other ones too.

Kind of loosely based on the paper "A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification" (https://arxiv.org/abs/2305.14752) which, I believe, was posted to HN not too long ago.