As indicated by the title, this paper is a discourse on  formal  methods, including comments about their value and use, an attempt to define the terminology, analogies with mathematics and cars, and speculation about the future. The definition of formal methods implied by the paper is the capability to reason formally about programs based on formal specifications. Although it is not a precise definition, it is probably generally acceptable. Some of the author’s other definitions, such as program validation meaning compilable, are not generally accepted.

The comments and analogies are good. The overall quality and length of the paper are reasonable. The reference list is not extensive. Four of the ten references are to the same issue of Computer Journal; three are to the next issue. I would recommend this paper as an easy-to-read commentary on formal methods for people familiar with formal methods.