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 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
prev sibling next sibling 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
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 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/


 . 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 reply BCS <none anon.com> writes:
Hello retard,

 the brick wall book by B.P.
 

link? -- ... <IXOYE><
Aug 01 2010
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 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.
 
 


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.
 



Added to the reading list... -- ... <IXOYE><
Aug 01 2010
prev sibling 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/


 . 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 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?

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?

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