4 ms·
> 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.
by cubefox 7mo 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?
- baq 7mo agoThe 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.
- jmalicki 7mo agoRoughly 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."