← Back to context

Comment by jmalicki

13 hours ago

I have experience with similar things!

But that's not saying the proofs are an issue - usually the spec you can reasonably prove in lean or another prover, say TLA+ or Z3 depending on your kind of program - has to be overly simplified and have a lot of assumptions.

However, that is powerful.

It doesn't mean your program doesn't have bugs.

It means this big scary complicated algorithm you think works but are skeptical doesn't have bugs - so when you encounter one, you know the bug is elsewhere, and you start really looking at the boundaries of what could be misspecified, if the assumptions given to the prover are actually true, etc.

It eliminates the big scary thing everyone will think is the cause of the bug as the actual cause.

This has been insanely valuable to me lately. It is also something I never really was able to do before the help of AI - vibe coding proofs about my programs is IMO one of the killer apps of AI, since there aren't a ton of great resources yet about how to do it well since it is rarely done.

4 comments

jmalicki

Reply
cubefox  4 hours ago

> This has been insanely valuable to me lately.

This surprises me. Formal verification so far has been a very niche thing apart from conventional type systems. I didn't think lack of vibe coding was much of a bottleneck in the past. Where do you use it?

  • jmalicki  26 minutes ago

    Roughly anything that, say, has the complexity of a leetcode medium level problem that isn't already an extremely well known algorithm.

    Any moderately complex thread safety thing with a few moving parts (e.g. there are multiple mutexes involved in various parts of the system, verify no deadlocks).

    The lack of vibe coding has been a bottleneck for literally everything before.

    When I see people say the hate vibe coding, I think "why do you hate formal verification? Because you could be spending your time on formal verification instead of removing "code smells" that don't hurt anything from vibe code."

  • baq  4 hours ago

    The problem is implementing anything approximately twice is a hard sell… this is no longer true, though - TLA+ models are cheap now. You should be using them when writing any sort of distributed systems, which is basically everything nowadays.