The ideal design and implementation of software systems should include detailed specifications of their requirements and functionalities. Unfortunately, as illustrated in this perceptive paper, writing software specifications without years of experience is taxing. What can computer scientists learn about software specifications from architects who design and oversee complex buildings? How can computer scientists educate the future generation of programmers to focus on the specifications of coding reliable programs?

Lamport clearly used examples from graph theory, systems optimizations, and concurrent and distributed systems to echo the need for students to understand the tasks of software components prior to writing application programs. Undeniably, formal program specifications support the proofs of correctness of programs. The standpoints in this article call for students to learn the art of program specifications through practice. Unfortunately, the time constraints imposed on course offerings at many college campuses make it problematic to provide the irreplaceable experiences of program specifications.

Clearly, Lamport never claimed to be a software security design expert in this article. Yet, I encourage all future designers of technologies to focus attention on the formal security specifications of hardware and software systems. But, do we have the adequate training environments as promoted by Lowry et al. [1] for educating future undergraduate and graduate computer scientists about the kinds of formal specifications advocated in this paper? You make the call.