I can't imagine removing this element of ambiguity because programs are not perfect. They are a representation of some mental process, and they frequently contain mistakes. They are also, as you admit, unable to capture states of the real world accurately. Unless your smart contract is unrelated to the real world (in which case, why bother with it?) this will be a problem.
The idea with formal verification is it would make it possible and feasible to prove a program is correct. But this is a hypothetical and until that is possible it doesn't really work. It might never be possible. So today I do agree with you. It just turns into a game of "ha-ha, you didn't read the contract closely enough!"