High quality human/computer interfaces have become a major topic of research. This paper describes a new method for modeling, designing, and developing dialogues, a method that has a strong formal basis and allows a uniform syntactic and semantic specification. This formal descriptive technique has the added advantage of being executable, that is, it has widely available translators. The technique chosen here allows a very high level specification of human/computer interaction enabling rapid development and easy modification. This paper describes the nature of the formal specifications written in first order logic using Prolog, and the successful specification and development of a carrier air traffic controller (CATC) dialogue. These experiments demonstrate the utility of Prolog as a high level specification language and point the way to a full dialogue development system that can incorporate a multi-layered concept of human/computer interaction.