Higher-order concurrent separation logic has been very successful in verifying correctness of intricate programs and reasoning about programming languages. In this talk we will present some basic ideas of program verification, separation logic, and how to use higher-order concurrent separation logic to reason about programs and programming languages. In particular, we will present and discuss the Iris program logic which is a general framework for defining separation logics and using them to reason about programs and programming languages.