There are no software practices that consistently lead to zero bugs. Not even formal verification. If someone says their favorite practice leads to zero bugs, you should immediately be deeply skeptical of how they define "zero" and "bugs".
29
65
412
Conversation
When I first heard about formal verification, I thought "Great! I can prove my code is correct and has no bugs." Soon after I realized I can only prove my program follows a specification, but it can't help me know whether the specification is the one I wanted.
2
15
Still incredibly useful! But definitely important to understand this limitation.
For sure! The same critique applies to type systems, especially as type systems get more expressive.
1
I'd also point out that specs are meant to be smaller, and they can be further validated by deriving theorems about behavior.
1