Re: At what point is a language so abstract that it simply cannot be compiled?

Martin Ward <>
Tue, 14 May 2019 12:52:44 +0100

          From comp.compilers

Related articles
| List of all articles for this month |

From: Martin Ward <>
Newsgroups: comp.compilers
Date: Tue, 14 May 2019 12:52:44 +0100
Organization: Compilers Central
References: 19-05-083
Injection-Info:; posting-host=""; logging-data="87760"; mail-complaints-to=""
Keywords: design
Posted-Date: 14 May 2019 12:57:53 EDT
In-Reply-To: 19-05-083

My WSL language is a "wide spectrum language" which includes
abstract specifications and low-level programming constructs in
the same language. At the specification level you can write
a specification statement of the form:

x := x'.Q

where x is a list of variable, x' is the corresponding list
of "primed variables" and Q is any formula of infinitary
first-order logic. If there is a set of values which can be assigned
to x' such that Q becomes true, then these values are assigned to x
and the statement terminates. (If there is more than one such
set of values, then one is selected nondeterminstically).
Otherwise, the statement aborts (does not terminate). For example:

<x> := <x'>.(x' = x + 1)

increments the value in x.

Since Q is a formula of infinitary first order logic,
the specification statement can be infinitely long.
There are formulae for which the solution cannot be computed:
for example, the Halting Problem for a Turing machine
can be implemented as a specification statement in WSL.

The language is used as the basis for my research into
program transformations. By using a wide-spectrum language
the refinement of a specification into exectuable code
is an example of a program transformation, as is the process
of reverse-engineering an abstract specification from
executable code.

A subset of WSL (not including the specification statement)
is implemented in the FermaT program transformation system:

The FermaT program transformation system is used commercially
to migrate assembler code to structured and maintainable
functionally equivalent high-level language code.

This paper includes an introduction to WSL and transformation theory:

"Pigs from Sausages? Reengineering from Assembler to C via
FermaT Transformations", M.Ward, Science of Computer Programming,
Special Issue on Program Transformation,
Vol 52/1-3, pp 213-255, 2004. ISSN 0167-6423

This paper discusses how the theory can be used to derive
algorithms from specifications to give a provably correct

"Provably Correct Derivation of Algorithms Using FermaT"
Martin Ward and Hussein Zedan
Formal Aspects of Computing, Volume 26, Issue 5, Pages 993–1031,
September 2014, ISSN 0934-5043

Copies of these papers and others are available on my web site:


Dr Martin Ward | Email: |
G.K.Chesterton site: | Erdos number: 4

Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.