A computer program should be written to never* deadlock, and that implies that the programmers have a vague proof sketch in their head of why it doesn't deadlock that could if needed be formalized as a proof.

*I'm sure there is some exception out there but it doesn't matter for this argument.