RaxcN's comments

On: Formal methods: Just good engineering practice?

[RaxcN]

The visible "productivity" as in manager friendly LOC. The actual productivity goes up.

Managers don't want that though, for reasons that already Dijkstra has outlined.

[xavxav → RaxcN]

I'm a researcher in formal verification; my thesis was building a tool to do this kind of stuff and I agree with the grandparent (though I would say probably closer to 5-10x slowdown not 100x).

Proofs are hard and often not for interesting reasons; its stuff like proving that you won't overflow a 2^64 counter which you only increment (aka something which won't happen for another couple billion years).

Current tools are only useful for specific kinds of problems in specific domains; things where a life really depends on correctness. Outside of those cases, lightweight techniques provide much more bang for your buck imo.

On: Formal methods: Just good engineering practice?

[RaxcN]

I do not know TLA+, but there is an abundance of other theorem provers that can model C very closely, including overflow, assignments, etc.

So closely, that when you transcribe such an algorithm to C, there is very little room for error, even if the C code isn't proven directly.

[rramadass → RaxcN]

> there is an abundance of other theorem provers that can model C very closely

Can you list some/all of them please? Would be helpful to others here.