Of course verification in its full generality is a dead end. However expressing an algorithm in a sound logical system, and proving properties of the algorithm

Of course verification in its full generality is a dead end. However expressing an algorithm in a sound logical system, and proving properties of the algorithm is quite fruitful. That's the approach taken by Coq and probably others. Most of the time the prover still needs some guidance from the user though.