プログラムの正しさとは？

プログラムと正しさ
プログラムにとっての「正しさ」って，なんだろう？　という点から出発し、数学における証明をプログラムに適用することを考えるも、最終的には現実路線に落ち着くお話。
夢かもしれないけれど、客観的に、手間暇かけずに、プログラムの正しさを検証する方法はないものか…。
いつも思うのですが、ソフトウェア開発って、角度を変えつつ同じものを3回作っていますよね。設計書としてシステムを作り(1回目)、設計書通りにプログラムを作り(2回目)、仕様書通り動作するか試験仕様書作って検証する(3回目)。
似たようなことは何度もやりたくない。どうやったら、3→1になるのか？　1に近づくのか？　まずは、2.9や2.8を目指すところからですね。