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.