In particular, I wanted to write about how a formal specification is different from a traditional program. But I think the existence of programming-language-like formal specification languages makes it even more important to drive home the difference between a program and a formal spec. The summary of this post is: a program is a list of instructions, a formal specification is a set of behaviors. And this is where formal specification languages come in: they allow us to define infinite sets of behaviors without having to explicitly enumerate every correct behavior. We just don’t care about the behaviors that are in the Property set but not in the Spec set.