A goal of programming language researches is to establish a method of developing efficient and correct programs with ease. However, it is generally difficult to chase these rabbits. Efficient programs are usually complicated and hence difficult to see correctness. In this talk, we study an approach to this problem based on program transformations. Program transformations enable us to derive complex programs from naive but apparently correct ones in a “correct by construction” manner. We see effectiveness of program transformations through examples, including deforestation, program inversion, and program parallelization.