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.

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.