Logogram strony

Myśliciel A.Rodin

Narodziny gwiazdy

Rozmiar tekstu

Why this project

It is a well-known fact that every user of a software application has to accept a disclaimer. Here is a typical example dating from 2018:

There is no warranty for the program, to the extent permitted by applicable law.  Except when otherwise stated in writing the copyright holders and/or other parties provide the program "as is" without warranty of any kind….

In my opinion, the cause of this situation is a lack of such mathematical models and tools for software engineers that would guarantee the functional reliability of products based on the way they have been designed and manufactured. The lack of mathematical models for programming languages also affects user-manuals of these languages which again contributes to low quality of programs.

In my opinion, the failure of constructing a practical system of gaining programs’ correctness has two sources.

The first lies in the fact that in building a programming language we start from syntax and only later — if at all — define its semantics. The second source is somehow similar but concerns programs: we first write a program and only then try to prove it correct.

To build a logic of programs for a programming language, one must first define its semantics on a mathematical ground. Since 1970-ties it was rather clear for mathematicians that such semantics to be “practical” must be compositional, i.e., the meaning of a whole must be a composition of the meanings of its parts. Later such semantics were called denotational — the meaning of a program is its denotation — and for about two decades researchers investigated the possibilities of defining denotational semantics for existing programming languages.

Unfortunately, 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 fact was unavoidable since for the existing programming languages a full denotational semantics simply cannot be defined. That was, in turn, the consequence of the fact that historically syntaxes were coming first and only later researchers were trying to give them a mathematical meaning. In other words — the decision of how to describe things was before what to describe.

The second group of problems followed from a tacit assumption that in the development of mathematically correct programs the development of programs should precede the proofs of their correctness. Although this order is quite obvious in mathematics — first theorem and then its proof — it is rather unusual for an engineer who usually first performs all necessary calculations (the proof) and only then builds his product.

As an attempt to cope with the mentioned problems I show in my book some mathematical methods that may be suitable for designing programming languages with denotational semantics. To illustrate the method an exemplary programming language, Lingua is developed from denotations to syntax. In this way, the decision of what to do (denotations) precedes the decision of how to express that (syntax).