プログラム導出とは、計算機科学において数学的手段を用いて仕様からプログラムを導き出すことである。プログラムを「導出」するとは、通常そのままでは実行不可能な形式的仕様を記述し、数学的に正しい規則を適用して実行可能なプログラムに変換することを意味する。このような手法で得られたプログラムは（最初の仕様にバグがない限り）構造的に正しいことが証明されている。形式的検証の場合、最初にプログラムを書き、それが与えられた仕様に照らして正しいことの証明を与える。この際の問題は以下の通りである。プログラム導出はそのような欠点を次のようにして改善する。プログラム導出とほぼ同義の用語として、transformational programming、algorithmics、deductive programming などがある。

出典:wikipedia