question

active

question:how-should-we-define-an-airline-reservation-for-the-purposes-of-an-elephant-reservation-program

How should we define an airline reservation for the purposes of an Elephant reservation program?

Better question about minimal definition for the program.

Source paper

extracted_from

Elephant 2000: A Programming Language Based on Speech Acts

McCarthy, John

Neighborhood — ranked by edge-count

Claims (1)

claim

This theory doesn't have to correspond exactly to human behavior or social customs; we only need analogs useful for program correctness.
gates
The speech act theory for programming can be simpler than human models.

Related by similarity (8)

cosine ≥ 0.65 · no typed edge

Entities in the same semantic neighborhood but without a typed relation to this one — candidates for new edges or unrecognized duplicates.

What is an airline reservation?question0.827
Question posed and then dismissed as the wrong question for program design.
What do we want to say about airline reservations to our program?question0.782
Question guiding minimal specification.
An airline reservation program's input-output specification is that it not order the admission of more passengers than the capacity of the flight. It is an external fact that the plane will hold its capacity and not more.claim0.779
Example distinguishing input-output and external facts.
Elephant programs that interact non-trivially with the outside world can have both input-output specifications, relating the programs inputs and outputs, and accomplishment specifications concerning what the program accomplishes in the world. These concepts are respectively generalizations of the philosophers' illocutionary and perlocutionary speech acts.claim0.725
Fifth abstract claim.
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.claim0.722
Sixth abstract claim.
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.claim0.710
Rejection of one of Dorschel's conditions for happy performance.
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.claim0.700
Fourth abstract claim.
Elephant 2000 programs can perform some kinds of speech acts as genuinely as humans, including genuine promises.claim0.697
McCarthy's position against Searle: computers can genuinely promise without requiring Searle's conditions (e.g., belief that fulfillment benefits recipient).