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
