www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Axiomatic purity of D

reply Justin Johansson <no spam.com> writes:
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
Jul 30 2010
next sibling parent Justin Johansson <no spam.com> writes:
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


obvious typo;
meant "... and to what degree *do* the naysayers believe ..."
Jul 30 2010
prev sibling next sibling parent reply lurker <lurk lurk.net> writes:
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.


What *is* axiomatic purity? A quick google books search returned titles like:

"Jesus remembered"
"American physics in transition: a history of conceptual change in"
"Feminism-art-theory: an anthology, 1968-2000"
"Feminism and tradition in aesthetics"
"Constructive interventions: paradigms, process and practice of .."
"Agriculture and rural connections in the Pacific, 1500-1900"
"Possessed by the past: the heritage crusade and the spoils of history"
Jul 30 2010
next sibling parent reply Justin Johansson <no spam.com> writes:
lurker wrote:

 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.


 
 What *is* axiomatic purity? A quick google books search returned titles like:
 
 "Jesus remembered"
 "American physics in transition: a history of conceptual change in"
 "Feminism-art-theory: an anthology, 1968-2000"
 "Feminism and tradition in aesthetics"
 "Constructive interventions: paradigms, process and practice of .."
 "Agriculture and rural connections in the Pacific, 1500-1900"
 "Possessed by the past: the heritage crusade and the spoils of history"
 


Well I never googled to see if my phrase was vernacular per se, though
on having googled for the exact phrase using bunny ear quotes, ie.
"axiomatic purity" I found this dubious title on page 2 of the Google
search results:

<search-result>
ACTION! Big Fuckin Tits, What is „Tits Granny“ and detailed. Tits Ass.
5 Jul 2010 ... Spoken in fulfilment - regardless newsreader to axiomatic 
purity! 3. Big hard tits. When blacken (or preciosity) she for him? ...
ww36.assandtits0adult.com/52-big-fuckin-tits.html - Cached
</search-result> LOL :-)

Nevertheless, I'm sure that readers of this NG would understand that
my reference to "axiomatic purity" in the context of the design of a
PL is in further reference to the formal mathematical/logical
soundness of the PL from a mathematical/logical axiomatic basis.

So for your further entertainment, would you please search on google
for the following phase (including quotes)
"axiomatic basis"
and report your findings back to this NG.

Kind regards,
Justin Johansson
Jul 30 2010
parent "Vladimir Panteleev" <vladimir thecybershadow.net> writes:
On Fri, 30 Jul 2010 17:10:28 +0300, Justin Johansson <no spam.com> wrote:


 Nevertheless, I'm sure that readers of this NG would understand that
 my reference to "axiomatic purity" in the context of the design of a
 PL is in further reference to the formal mathematical/logical
 soundness of the PL from a mathematical/logical axiomatic basis.


D is designed to be a practical, multi-paradigm programming language. As  
such, AFAIK it doesn't have any mathematical basis, except for as much you  
can say about const-correctness[1] and function purity[2]. Thus, I'd say  
"close to none".

   [1]: http://www.digitalmars.com/d/2.0/const-faq.html
   [2]: http://www.digitalmars.com/d/2.0/function.html#pure-functions

-- 
Best regards,
  Vladimir                            mailto:vladimir thecybershadow.net
Jul 30 2010
prev sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
lurker wrote:

 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.


 
 What *is* axiomatic purity? A quick google books search returned titles like:
 
 "Jesus remembered"
 "American physics in transition: a history of conceptual change in"
 "Feminism-art-theory: an anthology, 1968-2000"
 "Feminism and tradition in aesthetics"
 "Constructive interventions: paradigms, process and practice of .."
 "Agriculture and rural connections in the Pacific, 1500-1900"
 "Possessed by the past: the heritage crusade and the spoils of history"
 


It's safety, which requires two proofs: progress and preservation. I 
found this excerpt from a book I'd recommend:

http://books.google.com/books?id=ti6zoAC9Ph8C&pg=PA95&lpg=PA95&dq=safety+%3D+progress+%2B+preservation&source=bl&ots=EzM9xEpZWD&sig=CJrn0iCMOCrBk_YF9CvXn-2GG60&hl=en&ei=nnJTTIyREoigsQPY8JXaAg&sa=X&oi=book_result&ct=result&resnum=1&ved=0CBIQ6AEwAA#v=onepage&q=safety%20%3D%20progress%20%2B%20preservation&f=false


Andrei
Jul 30 2010
parent Justin Johansson <no spam.com> writes:
Andrei Alexandrescu wrote:

 lurker wrote:

 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.


 What *is* axiomatic purity? A quick google books search returned 
 titles like:

 "Jesus remembered"
 "American physics in transition: a history of conceptual change in"
 "Feminism-art-theory: an anthology, 1968-2000"
 "Feminism and tradition in aesthetics"
 "Constructive interventions: paradigms, process and practice of .."
 "Agriculture and rural connections in the Pacific, 1500-1900"
 "Possessed by the past: the heritage crusade and the spoils of history"


 
 It's safety, which requires two proofs: progress and preservation. I 
 found this excerpt from a book I'd recommend:
 
 http://books.google.com/books?id=ti6zoAC9Ph8C&pg=PA95&lpg=PA95&dq=safety+%3D+progress+%2B+preservation&source=bl&ots=EzM9xEpZWD&sig=CJrn0iCMOCrBk_YF9CvXn-2GG60&hl=en&ei=nnJTTIyREoigsQPY8JXaAg&sa=X&oi=book_result&ct=result&resnum=1&ved=0CBIQ6AEwAA#v=onepage&q=safety%20%3D%20progress%20%2B%20
reservation&f=false 
 
 
 
 Andrei


Thanks for the recommendation; going by the 11/12 positive reader
comments from that link as well, this book has been added to my
reading list.

Justin
Aug 01 2010
prev sibling next sibling parent Justin Johansson <no spam.com> writes:
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


On the question of whether or not having an axiomatic backing for a PL
matters, I happened across this interesting article by Tony Hoare.

<<
Retrospective: An Axiomatic Basis for Computer Programming

C.A.R. Hoare revisits his past Communications article on the axiomatic 
approach to programming and uses it as a touchstone for the future.

http://cacm.acm.org/magazines/2009/10/42360-retrospective-an-axiomatic-basis-for-computer-programming/fulltext




Justin Johansson



 Jul 30 2010



prev sibling  parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org>  writes:


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



 Aug 01 2010



 next sibling parent reply Jonathan M Davis <jmdavisprog gmail.com>  writes:


On Sunday 01 August 2010 14:13:40 Andrei Alexandrescu wrote:

 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.


Thanks to reflection, it wouldn't be all that hard to shove the wrong type into
a 
container with code that can't be properly checked at compile time. Since all 
the generic stuff is simply compile-time checks, the compiler fails to catch
the 
problem, and all of the code which compiled with the assumption that the
objects 
in the container were all of one type will fail when it goes to get the item 
with the wrong type out of the container. I think that all of the casts are 
still there though (since technically, the container holds Objects not the 
specific type). It's just that they aren't in the user code.

In reality, this sort of thing pretty much doesn't happen, because you have to 
go out of your way to make it happen, but as far as proofs go, it's definitely 
going to fail.

- Jonathan M Davis



 Aug 01 2010



 next sibling parent reply retard <re tard.com.invalid>  writes:


Sun, 01 Aug 2010 16:02:56 -0700, Jonathan M Davis wrote:


 On Sunday 01 August 2010 14:13:40 Andrei Alexandrescu wrote:

 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.


 
 Thanks to reflection, it wouldn't be all that hard to shove the wrong
 type into a container with code that can't be properly checked at
 compile time. Since all the generic stuff is simply compile-time checks,
 the compiler fails to catch the problem, and all of the code which
 compiled with the assumption that the objects in the container were all
 of one type will fail when it goes to get the item with the wrong type
 out of the container. I think that all of the casts are still there
 though (since technically, the container holds Objects not the specific
 type). It's just that they aren't in the user code.
 
 In reality, this sort of thing pretty much doesn't happen, because you
 have to go out of your way to make it happen, but as far as proofs go,
 it's definitely going to fail.
 
 - Jonathan M Davis


If you restrict yourself to a subset of the language with no casts and no 
pointer manipulation, all kind of safety properties of the polymorphic / 
generic containers can be proven. There is even a "safe" version of casts 
known as pattern matching in languages like Scala. However, if the class 
hierarchy isn't sealed, one cannot prove whether the pattern matching 
function is total. There are also other issues with patterns because of 
the type erasure in JVM.

Sounds like Andrei might have read the brick wall book by B.P. It's a 
basic book about language design (orthogonal to the parsing/backend books 
like the one with the dragon in its cover) and an essential part of grad/
postgrad studies in many places. It's a good read they say.



 Aug 01 2010



 next sibling parent  retard <re tard.com.invalid>  writes:


Sun, 01 Aug 2010 23:33:38 +0000, retard wrote:


 Sun, 01 Aug 2010 16:02:56 -0700, Jonathan M Davis wrote:
 

 On Sunday 01 August 2010 14:13:40 Andrei Alexandrescu wrote:

 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.


 
 Thanks to reflection, it wouldn't be all that hard to shove the wrong
 type into a container with code that can't be properly checked at
 compile time. Since all the generic stuff is simply compile-time
 checks, the compiler fails to catch the problem, and all of the code
 which compiled with the assumption that the objects in the container
 were all of one type will fail when it goes to get the item with the
 wrong type out of the container. I think that all of the casts are
 still there though (since technically, the container holds Objects not
 the specific type). It's just that they aren't in the user code.
 
 In reality, this sort of thing pretty much doesn't happen, because you
 have to go out of your way to make it happen, but as far as proofs go,
 it's definitely going to fail.
 
 - Jonathan M Davis


 
 If you restrict yourself to a subset of the language with no casts and
 no pointer manipulation, all kind of safety properties of the
 polymorphic / generic containers can be proven. There is even a "safe"
 version of casts known as pattern matching in languages like Scala.
 However, if the class hierarchy isn't sealed, one cannot prove whether
 the pattern matching function is total. There are also other issues with
 patterns because of the type erasure in JVM.
 
 Sounds like Andrei might have read the brick wall book by B.P. It's a
 basic book about language design (orthogonal to the parsing/backend
 books like the one with the dragon in its cover) and an essential part
 of grad/ postgrad studies in many places. It's a good read they say.


My bad, didn't open the link above until now.



 Aug 01 2010



prev sibling  parent reply BCS <none anon.com>  writes:


Hello retard,


 the brick wall book by B.P.
 


link?

-- 
... <IXOYE><



 Aug 01 2010



 next sibling parent reply retard <re tard.com.invalid>  writes:


Sun, 01 Aug 2010 23:42:55 +0000, BCS wrote:


 Hello retard,
 

 the brick wall book by B.P.
 
 


 link?


The link was on another reply in this thread:

http://books.google.com/books?id=ti6zoAC9Ph8C&pg=PA95&lpg=PA95&dq=safety+%
3D+progress+%2B
+preservation&source=bl&ots=EzM9xEpZWD&sig=CJrn0iCMOCrBk_YF9CvXn-2GG60&hl=en&ei=nnJTTIyREoigsQPY8JXaAg&sa=X&oi=book_result&ct=result&resnum=1&ved=0CBIQ6AEwAA#v=onepage&q=safety
%20%3D%20progress%20%2B%20preservation&f=false

or

http://www.cis.upenn.edu/~bcpierce/tapl/



 Aug 01 2010



  parent  BCS <none anon.com>  writes:


Hello retard,


 Sun, 01 Aug 2010 23:42:55 +0000, BCS wrote:
 

 Hello retard,
 

 the brick wall book by B.P.
 


 link?
 


 The link was on another reply in this thread:
 


Added to the reading list...

-- 
... <IXOYE><



 Aug 01 2010



prev sibling  parent  Justin Johansson <no spam.com>  writes:


BCS wrote:

 Hello retard,
 

 the brick wall book by B.P.


 
 link?
 


I think the OP means Types and programming languages
  By Benjamin C. Pierce

Andrei posted the link earlier in this thread.

http://books.google.com/books?id=ti6zoAC9Ph8C&pg=PA95&lpg=PA95&dq=safety+%3D+progress+%2B+preservation&source=bl&ots=EzM9xEpZWD&sig=CJrn0iCMOCrBk_YF9CvXn-2GG60&hl=en&ei=nnJTTIyREoigsQPY8JXaAg&sa=X&oi=book_result&ct=result&resnum=1&ved=0CBIQ6AEwAA#v=onepage&q=safety%20%3D%20progress%20%2B%20preservation&f=false



 Aug 01 2010



prev sibling  parent  Andrei Alexandrescu <SeeWebsiteForEmail erdani.org>  writes:


On 08/01/2010 06:02 PM, Jonathan M Davis wrote:

 On Sunday 01 August 2010 14:13:40 Andrei Alexandrescu wrote:

 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.


 Thanks to reflection, it wouldn't be all that hard to shove the wrong type
into a
 container with code that can't be properly checked at compile time.


Good point. Reflection is commonly avoided in the kind of formal proofs 
I mentioned.

Andrei



 Aug 01 2010



prev sibling  parent reply Justin Johansson <no spam.com>  writes:


Andrei Alexandrescu wrote:

 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?


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


While being somewhat disappointed that this topic has not gathered much
momentum, my thoughts are now that it was an ill-conceived question.
Certainly I am not well enough read about type systems and my guess
is that not many others on this readership are either.

I am interested to know however what the last respondent's exact
motive was to delay answering the question until after others had.
Admittedly we all often hold back to see what others are saying
first so by no means I am inferring any criticism here.

Cheers
Justin Johansson



 Aug 02 2010



  parent  Andrei Alexandrescu <SeeWebsiteForEmail erdani.org>  writes:


On 08/02/2010 08:00 AM, Justin Johansson wrote:

 Andrei Alexandrescu wrote:

 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?


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


 While being somewhat disappointed that this topic has not gathered much
 momentum, my thoughts are now that it was an ill-conceived question.
 Certainly I am not well enough read about type systems and my guess
 is that not many others on this readership are either.

 I am interested to know however what the last respondent's exact
 motive was to delay answering the question until after others had.
 Admittedly we all often hold back to see what others are saying
 first so by no means I am inferring any criticism here.


Not much to read into it - I was just curious how interested people are 
in the topic.

Andrei



 Aug 02 2010