Programmtransformation charakterisiert eine Methodik der Softwareentwicklung bei der man aus einer formalen, meist funktional-deklarativen Spezifikation durch schrittweise Anwendung semantiktreuer Umformungsregeln ein Programm ableitet, das nicht nur per Konstruktion korrekt ist, d.h. die Spezifikation erfüllt, sondern auch weiteren wichtigen Kriterien wie etwa Effizienz genügen kann.
Konkretes Ergebnis der Anwendung dieses Ansatzes auf die funktionale Programmierung ist das interaktive, prototypische Transformationssystem Ultra, das eine gute Basis für weitere Studien im Rahmen der formalen Programmentwicklung bietet.