In 1969 Edsger W.Dijkstra, one of the founders of computer science, wrote: "it is not only the programmer's task to produce a correct program but also to demonstrate its correctness in a convincing manner". He continued: "program correctness is not my only concern, program adaptability or manageability will be another". Following this approach, most modern programming languages are designed with features that make it easier to understand, test, modify, and maintain programs. Such features, however, often result in additional memory usage and/or slower programs. Often these costs can be offset by tools that automatically optimize programs. Program optimization, however, is a non-trivial task since changes to a program must be performed without changing the behavior of the program. In this talk I will discuss some features of modern programming languages and their effect on performance. I will give an overview of my research on proving that certain program transformations preserve programs' behavior. I will also discuss a program optimization developed with my students for the widely-used Java programming language.