I will report on some experience in the application of formal methods to software engineering, including a puzzling semantic problem related to rep exposure that has not yet received as much attention as it deserves. I will also make some general remarks about the relationship between software engineering and foundational theories of formal methods.