Axiomatic purity of D

[Andrei Alexandrescu]

On 07/30/2010 08:02 AM, Justin Johansson wrote:
> To what degree do the author and advocates of the D(2) Programming
> Language believe that it is axiomatically pure and to what degree
> to the naysayers believe that it is conversely impure. Further,
> does axiomatic purity in a PL really matter?
>
> Thanks in advance for all opinions offered.
>
> Cheers
> Justin Johansson

I wanted to answer this question after others have, but it seems the 
topic hasn't garnered a lot of attention.

Proving soundness for a language entails proving two theorems: progress 
and preservation. The theorems are usually proven against a collection 
of constructs called the operational semantics of the language, which 
express the operations defined by the language and their effects. There 
are two kinds of operational semantics - big step and small step. All 
soundness proofs I saw were on the small step operational semantics.

In a nutshell, proving progress is proving that any program in the 
analyzed language either terminates (usually yielding a value) or can 
take a step. In other words, no program can get in a "stuck" state where 
it can't take a step. Traditional examples of stuck states are division 
by zero, out of bounds access, or null pointer dereference.

Proving preservation is proving that after any step taken in evaluating 
a term in the analyzed language, the type of the term remains unchanged.

Both proofs are typically large by-case inductions. Because proofs for 
real languages would be very large, proofs focus on synthetic, reduced 
languages that are designed to minimize the number of constructs while 
still keeping the language's fundamental properties.

Most languages have not been proven sound. I know ML has been, and there 
is a reduced version of Java (Featherweight Java) that has been proven 
sound. I know that Java with generics has been shown unsound a long time 
ago 
(http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00849.html). 
I haven't followed to see whether that issue has been fixed. My 
understanding is that as of this time Java with generics is still 
unsound, i.e. there are programs without casts that produce type errors 
at runtime.

On to D's soundness. I think full D is impossible to prove sound (due to 
casts, unsafe functions, and direct access to memory) without making 
certain assumptions. What I think is feasible and valuable is proving 
that certain features of D are sound. For example, I think it's not 
difficult to prove that immutable is really immutable. A much more 
involved proof would define SafeD as a subset of D and then prove its 
soundness.

I'm not an expert on formal proofs; it has been my research focus in my 
first years in grad school, and I haven't gotten to the point where I 
was conversant with formalisms enough to produce interesting proofs. I 
could understand one, and if I find the time and perhaps a collaborator 
I'd be glad to work on formally proving certain properties of D.


Andrei