Proving that a program fulfills its commitments seems to be just a matter of expressing a commitment as making sure a certain sentence is true, e.g. that the passenger is allowed on the airplane. In that case, proving that the program fulfills its commitments is just a matter of showing that the sentences expressing the commitments follow from the sentence expressing the program. The problem now is to decide what class of sentences to allow as expressing various kinds of commitments. If the commitments are to be externally expressed as promises, then they have to belong to the i-o language.
Commitments are like specifications, but they are to be considered as dynamic, i.e. specific commitments are created as the program runs. It makes sense to ask what are the program's commitments when it is in a given state. Indeed some programs should be written so as to be able to answer questions about what their commitments are.
An Elephant interpreter need only match the inputs against the program statements with inputs as premises. It then issues the outputs, performs the actions and asserts the other conclusions of the statement. The circumscriptions should not have to be consulted, because they can be regarded as asserting that the only events that occur are those specified in the statements. Here the situation is similar to that of logic programming. The circumscriptions are used in proving that the program meets its specifications, e.g. fulfills its commitments.
There is a theorem about this that remains to be precisely formulated and then proved. Making it provable might involve some revisions of the formalism.
Many kinds of human speech act are relative to social institutions that change. For example, a challenge to a duel in societies where dueling was customary was not just an offer. It generated certain obligations on the part of the challenger, the person challenged and the community. Suppression of dueling was accomplished partly by intentional changes in these institutions. The exchange of speech acts among computer programs will often involve the design of new institutions prescribing the effects of speech acts. For example, the kinds of external obligation created by business promises is partially specified by the Uniform Commercial Code that many states have enacted into law. Programs that make commitments will have to be specified in some way that corresponds to something like the Uniform Commercial Code. One point is to be able to prove that (subject to certain assumptions) the programs do what is legally required. Another is that the effects of commercial speech acts should be defined well enough for programs to keep track of the obligations they have incurred and the obligations incurred to them. The simplest case is keeping track of the effects of the speech acts on accounts receivable and accounts payable.
Perhaps we will need three levels of specification, internal, input-output and accomplishment. Internal specifications may involve computing a certain quantity, regardless of whether output occurs.
Some communications among parts of a program may also usefully be treated as speech acts.
We may need to consider joint speech acts such as making an agreement. For some purposes an agreement can be considered as an offer followed by its acceptance. However, we may know that two parties made an agreement without knowing who finally offered and who finally accepted.
It seems that (Searle and Vanderveken 1985) improves on (Searle 1969) in distinguishing successful and non-defective performance of speech acts. It isn't clear whether these distinctions will play a role in computer speech acts. Perhaps the logic of illocutionary acts proposed in that book will be useful in writing specifications and proving that programs meet them.
Writing this paper began with the simple notion of a program that makes commitments and the notion of proving that it fulfills them. Then it became interesting to consider speech acts with more elaborate correctness conditions. However, we expect that the simple cases will be most useful in the initial applications of Elephant 2000 and similar languages.
Dorschel (1989) proposes certain conditions for the ``happy'' performance of directive speech acts, e.g. orders, promises and declarations. It turns out we want some of them and not others. By this I mean that when someone verifies an Elephant program, he will want to show that some of Dorschel's conditions are satisfied and not others.
For example, Dorschel proposes that a promise being fulfilled necessitates that making the promise be a cause of the act that fulfills it. The Elephant programmer in verifying his program need not show that the promise will be fulfilled because it was made. It is enough that he show it will be fulfilled. On the other hand, Dorschel proposes to require that an order is properly made only if the speaker has authority to give the order. We'll surely want that--especially for purchase orders, which include both an order component and a promise component.
These considerations illustrate our right to pick and choose among the concepts proposed by philosophers.