paper
active
paper:2021-10-16-stefan-lesser-elephant-pdf-26c323

Elephant 2000: A Programming Language Based on Speech Acts

ByJohn McCarthyStanford University
Denotational & semantic program designDenotational & semantic program designAbstract PerformativesAlgol 48knows-what formalizationAccomplishment SpecificationAlgol 50"An elephant never forgets!""An elephant's faithful, one hundred percent!"authoritycommitmentcommon sense informatic situationdirect reference to the pasthappiness conditionsI-O languageIllocutionary Acts+12 more

TL;DR

Elephant 2000, a programming language proposed by John McCarthy at Stanford, establishes that program correctness can be partially defined through the semantics of speech acts—specifically that programs can be held to standards of truthfulness, responsiveness, and commitment-fulfillment without requiring Hoare axioms or a separate theory of programming. The language introduces abstract performatives as its core instrument: formal analogs of Austin's (1962) and Searle's (1969) illocutionary acts—requests, promises, commitments, questions, answers, permissions—whose correctness conditions are automatically derivable from program text as logical sentences. Programs are themselves logical sentences (or syntactic sugarings thereof), a design illustrated through the intermediate languages Algol 48 and Algol 50, which represent Algol 60 fragments as recursion equations over explicit time indices; correctness of the Algol 50 multiplication program, for instance, is expressed as a universally quantified sentence provable from the program sentences plus Peano arithmetic alone. The language targets transaction processing and electronic data interchange applications—including the X12 standard and McCarthy's 1982 Common Business Communication Language (CBCL)—where programs belonging to different organizations must exchange obligations. A key design decision is that Elephant source programs can refer directly to the past via a virtual history list, eliminating the need for explicit data structures in source code while leaving compilers (targeting Common Lisp or C) to generate appropriate object-level structures. The paper argues this implies that program verification in commercial and inter-organizational settings can proceed from first-order logic alone, that illocutionary and perlocutionary correctness conditions correspond precisely to input-output versus accomplishment specifications, and that the philosophical complexities of obligation can be largely bypassed by specifying only whether commitments are fulfilled.

What to take away

  1. 1. Elephant 2000 programs are themselves logical sentences (or statement-by-statement syntactic sugarings of logical sentences), so their extensional correctness properties follow as logical consequences without requiring Hoare axioms or any intervening theory of programming.
  2. 2. The language introduces abstract performatives—internal commitments, promises, requests, questions, acceptances—as first-class program constructs whose correctness conditions (truthfulness, responsiveness, commitment-fulfillment) can be generated automatically from program text.
  3. 3. The correctness of the Algol 50 multiplication program is expressed as the sentence ∀mn(n≥0 ⊃ ∀t(pc(t)=0 ⊃ ∃t′(t′>t ∧ pc(t′)=6 ∧ p(t′)=mn))), provable from the program's recursion equations plus standard Peano arithmetic with no special programming logic.
  4. 4. Elephant source programs eliminate explicit data structures by referring directly to the past via a virtual history list; a compiler targeting Common Lisp or C constructs necessary object-level data structures automatically.
  5. 5. The illocutionary/perlocutionary distinction maps directly onto input-output specifications (verifiable from program semantics alone) versus accomplishment specifications (requiring axioms about the physical world), as illustrated by an airline reservation program and an air traffic control program.
  6. 6. An airline reservation in Elephant 2000 is expressed using commitment, make, exists, and cancel as primitive Elephant-defined operations, with fullness defined as card{psgr | exists commitment admit(psgr,flt)} = capacity flt, requiring no separate reservation data structure.
  7. 7. Responsiveness of answers—beyond mere truthfulness—requires a logical apparatus using separate notations for objects and concepts (from McCarthy 1979b), formalized as knows-what(pat, Telephone Mike) ≡ ∃x(telephone-number x ∧ knows-that(pat, Equal(Telephone Mike, Concept1 x))).
  8. 8. The paper raises the open question of whether a theorem guaranteeing that circumscribing the arises, outputs, and revoke predicates correctly limits program behavior to specified events can be precisely formulated and proved, noting this 'remains to be precisely formulated and then proved.'
  9. 9. A replicable methodology choice: Algol 48 represents Algol 60 programs as recursion equations over three explicit time-indexed functions—p(t), i(t), pc(t)—sorted by variable rather than sequentially by time, yielding a statement-by-statement syntactic transformation to logical sentences.
  10. 10. McCarthy argues that Elephant 2000 programs can perform speech acts 'as genuinely as do humans,' directly contesting Searle's (1984) position that computers cannot really promise, on the grounds that human institutional speech acts (e.g., giving a reservation) are themselves often stripped of the full intentional conditions Searle requires.

Peer brief — for seminar discussion

McCarthy's Elephant 2000 paper, originating in 1989 and revised through 1994, proposes a programming language whose defining feature is that communication inputs and outputs are meaningful speech acts in the sense of Austin (1962) and Searle (1969), and that program correctness is partly constituted by the proper performance of those acts. The primary mechanism introduced is the abstract performative—an internal commitment, promise, request, permission, or answer that carries correctness conditions derivable automatically from program text as first-order logical sentences. Because Elephant programs are themselves logical sentences (or syntactic sugarings reducible statement-by-statement to logical sentences), their properties follow directly from those sentences plus domain axioms, making Hoare-style proof systems or separate theories of programming unnecessary. This is first demonstrated through two intermediate languages, Algol 48 and Algol 50: Algol 48 encodes an Algol 60 multiplication loop as recursion equations over explicitly time-indexed variables p(t), i(t), pc(t), and the correctness statement ∀mn(n≥0 ⊃ ∀t(pc(t)=0 ⊃ ∃t′(t′>t ∧ pc(t′)=6 ∧ p(t′)=mn))) is proved from those equations and Peano arithmetic alone. Algol 50 extends this with reified state vectors using McCarthy's (1963) assignment and contents functions a(var,val,ξ) and c(var,ξ). The main load-bearing finding is that this architecture scales to interactive programs: an airline reservation program is fully expressible using commitment, make, exists, and cancel as primitives—with flight fullness defined as card{psgr | exists commitment admit(psgr,flt)} = capacity flt—and no explicit reservation data structure in source code. The paper further distinguishes input-output specifications (illocutionary, verifiable from program semantics alone) from accomplishment specifications (perlocutionary, requiring world axioms), arguing both should be formulated and related for any non-trivial interactive program. The target application domain is electronic data interchange and transaction processing, specifically situations like X12 standard document exchange and the Common Business Communication Language proposed in McCarthy (1982), where programs belonging to independent organizations must exchange legally binding obligations with minimal human supervision. An alternative formal approach the paper could have used—and explicitly rejects—is temporal logic, which Francez and Pnueli (1978) employed for cyclic programs; McCarthy argues temporal logic is too weak to express many important program properties compared to explicit time in first-order logic. The most contestable aspect is the paper's claim that Elephant programs can perform speech acts 'as genuinely as do humans,' which is asserted as a rebuttal to Searle (1984) but rests on the design-stance argument from Dennett (1971) rather than any formal result—a critical reader would press hard on whether stripping speech acts of their full intentional and institutional conditions (sincerity, authority, legal obligation) produces genuine speech acts or merely a useful formal simulacrum, and whether the automatic generation of intrinsic correctness conditions from program text has been demonstrated beyond the toy reservation example. The paper also acknowledges that a key theorem—that circumscribing arises, outputs, and revoke correctly restricts program behavior to specified events, analogously to the closed-world assumption in logic programming—'remains to be precisely formulated and then proved,' leaving the formal foundations of the compiled implementation incomplete.

Methods (1)

  • knows-what formalization
    A logical definition using Concept1 to formalize knowing the answer, for specifying responsiveness.

Frameworks (2)

  • Algol 48
    Hypothetical preliminary version of Algol 50 using recursion equations and explicit time; illustrates representation of programs as logical sentences.
  • Algol 50
    Hypothetical programming language using reified variables and state vectors as warmup for representing Elephant programs as logical sentences.

Findings (1)

Claims (34)

Hypotheses (4)

Questions (8)

Related work— refs + corpus + external arXiv

Cited / in-corpus / arXiv badges show which signals surfaced each row. Multi-source rows weighted higher.

+16 more

Similar preprints — Semantic Scholar

Cross-corpus bridges (1)

same_concept_as · Nomic cosine

External markdown files that talk about the same concept as this entity.

  • alexander
    Elephant 2000: A Programming Language Based on Speech Actspapers/extracted/2021-10-16_Stefan-Lesser_elephant.pdf_26c323.md0.888