alt Hacker News> 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?
Replies
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."
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.