A proposal of a seminar

Utworzono: poniedziałek, 29 kwiecień 2019 16:58

Poprawiono: środa, 01 maj 2019 12:11

Odsłony: 5678

An experiment with denotational semantics (reversing the traditional order of things)  Download the presentation

The lecture in the minimal size (60 min) covers slides 1 to 15 of the presentation. For a full version ca. 120 min would be necessary plus an appropriate time for a discussion.

The problem of mathematically-provable program-correctness appeared for the first time in a work of Alan Turing published in conference proceedings On High-Speed Calculating Machines (Cambridge 1949). Later, for several decades, that subject was investigated usually as proving program correctness, but the developed methods never became everyday tools of software engineers. Finally, all these efforts were abandoned what has been emphatically stated in 2016 by the authors of a monography Deductive Software Verification:

In the last years, it became more and more clear that full functional verification is an elusive goal for almost all application scenarios.

To guarantee program correctness we need a program logic, and to build such logic, we need a mathematical semantics of our language. In my opinion, the failure of building practical logics based on mathematical semantics has two sources.

First concerns the approach to defining semantics, second — to making programs correct.

Since 1970-ties it was rather clear for mathematicians that semantics to be “practical” must be denotational, i.e., the meaning of a whole must be a composition of the meanings of its parts. Although for about two decades researchers investigated the possibilities of defining denotational semantics for existing programming languages, none of these attempts resulted in the creation of software-engineering tools that would be widely accepted by the IT industry. In my opinion that was unavoidable since for the existing programming languages a practical denotational semantics simply cannot be defined. This, in turn, is the result of first defining the syntax, and only later its meaning. In other words, we first decide how we are going to talk, and only later ? what we are going to talk about.

The second source of problems is somehow similar but concerns programs: we first write an (incorrect) program and then try to prove it correct.

In my experiment, I suggest reversing both orders. First, a language is built from denotations to syntax, which — as it turns out — guarantees the existence of its denotational semantics. Second, the logic of programs is not used to prove the correctness of programs, but to develop programs in a way that guarantees their correctness. The traditional mathematical philosophy — first a hypothesis, then its proof — is replaced by an engineer’s perspective who in designing and constructing a bridge uses tools (also mathematical) which guarantee that the bridge will not collapse.

Persons interested in the details of the approach are referred to The book.