Elephant 2000 is a proposed programming language good for writing and verifying programs that interact with people (e.g. transaction processing) or interact with programs belonging to other organizations (e.g. electronic data interchange)
Communication inputs and outputs are in an I-O language whose
sentences are meaningful speech acts identified in the language as
questions, answers, offers, acceptances, declinations, requests,
permissions and promises.
The correctness of programs is partly defined in terms of proper performance of the speech acts. Answers should be truthful and responsive, and promises should be kept. Sentences of logic expressing these forms of correctness can be generated automatically from the form of the program.
Elephant source programs may not need data structures, because they can refer directly to the past. Thus a program can say that an airline passenger has a reservation if he has made one and hasn’t cancelled it.
Elephant programs themselves can be represented as sentences of logic. Their extensional properties follow from this representation without an intervening theory of programming or anything like Hoare axioms.
Elephant programs that interact non-trivially with the outside world can have both {\it input-output specifications}, relating the programs inputs and outputs, and {\it accomplishment specifications} concerning what the program accomplishes in the world. These concepts are respectively generalizations of the philosophers’ {\it illocutionary} and {\it perlocutionary} speech acts.
Programs that engage in commercial transactions assume obligations on behalf of their owners in exchange for obligations assumed by other entities. It may be part of the specifications of an Elephant 2000 programs that these obligations are exchanged as intended, and this too can be expressed by a logical sentence.
Human speech acts involve intelligence. Elephant 2000 is on the borderline of AI, but the article emphasizes the Elephant usages that do not require AI. \end{enumerate}
John McCarthy has been Professor of Computer Science at Stanford University since 1962. His research is mainly in artificial intelligence. Long ago he originated the Lisp programming language and the initial research on general purpose time-sharing computer systems. More can be found in his Web page John McCarthy’s home page. As a public service, he has created a Web page on the sustainability of material progress. Material progress is indeed sustainable.
For information on exhibition and sponsorship opportunities at the conference, contact Yvonne Romaine.
Download the ETech Sponsor/Exhibitor Prospectus
Download the Media & Promotional Partner Brochure (PDF) for more information on trade opportunities with O'Reilly conferences, or contact Avila Reese at mediapartners@oreilly.com.
For media-related inquiries, contact confpr@oreilly.com.
To stay abreast of conference news and to receive email notification when registration opens, please sign up for the ETech newsletter (login required).
View a complete list of ETech contacts.