<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Rather than denotationally, I'd emphasise the axiomatic foundations of GCL in terms of wp.<div>Whilst EWD had plenty to say about programming languages his over arching concern was programming methodology and the implementation</div><div>of correct programs wrt a specification.</div><div>It is not just a matter of simpler semantics.  In <span style="color:rgba(0,0,0,0.901961);font-family:-apple-system,system-ui,BlinkMacSystemFont,"Segoe UI",Roboto,"Helvetica Neue","Fira Sans",Ubuntu,Oxygen,"Oxygen Sans",Cantarell,"Droid Sans","Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol","Lucida Grande",Helvetica,Arial,sans-serif;white-space:pre-line">EWD798 Dijkstra writes that (at the event) he gave a correctness proof  that went against the assumption that applicative programs are easier to prove correct than imperative ones.  I believe he repeats that comment elsewhere though I can't find a reference. (I was curious to find what the algorithm was that he presented. I tried emailing a few people whom I thought might have been at the meeting,</span></div><div><span style="color:rgba(0,0,0,0.901961);font-family:-apple-system,system-ui,BlinkMacSystemFont,"Segoe UI",Roboto,"Helvetica Neue","Fira Sans",Ubuntu,Oxygen,"Oxygen Sans",Cantarell,"Droid Sans","Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol","Lucida Grande",Helvetica,Arial,sans-serif;white-space:pre-line">unfortunately no one had notes or could recall. The event was </span><span style="color:rgb(0,0,0);font-family:-webkit-standard;font-size:medium">"Advanced Course on Functional Programming and its Applications" 1981.Whilst I believe on the basis of the EWD'staDijkstra thought highly of FP in</span></div><div><span style="color:rgb(0,0,0);font-family:-webkit-standard;font-size:medium">that it supported the  style of calculational proof/development  that he advocated, I don't believe that he saw FP as a 'silver bullet' or necessarily the best option. And </span></div><div><span style="color:rgb(0,0,0);font-family:-webkit-standard;font-size:medium">his</span></div><div><span style="color:rgb(0,0,0);font-family:-webkit-standard;font-size:medium">support for Haskell must be seen in the  context of a discussion on alternatives for a programming course rather than advocacy per se. Indeed he was careful to write:</span></div><div><span style="font-family:-webkit-standard;color:rgb(0,0,0);font-size:medium;text-indent:32px">inally, in the specific comparison of Haskell versus Java, "Haskell, though not perfect, is of a quality that is several orders of magnitude higher than Java, which is a mess" </span><span style="color:rgb(0,0,0);font-family:-webkit-standard;font-size:medium"><br></span></div><div><span style="font-family:-webkit-standard;color:rgb(0,0,0);font-size:medium;text-indent:32px">[Dijkstra "</span><u style="font-family:-webkit-standard;color:rgb(0,0,0)">To the members of the Budget Council" 12 April 2001.</u></div><div><span style="color:rgb(0,0,0);font-family:-webkit-standard;font-size:medium"><br></span></div><div><span style="color:rgba(0,0,0,0.901961);font-family:-apple-system,system-ui,BlinkMacSystemFont,"Segoe UI",Roboto,"Helvetica Neue","Fira Sans",Ubuntu,Oxygen,"Oxygen Sans",Cantarell,"Droid Sans","Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol","Lucida Grande",Helvetica,Arial,sans-serif;white-space:pre-line">Indeed</span></div><div><span style="color:rgba(0,0,0,0.901961);font-family:-apple-system,system-ui,BlinkMacSystemFont,"Segoe UI",Roboto,"Helvetica Neue","Fira Sans",Ubuntu,Oxygen,"Oxygen Sans",Cantarell,"Droid Sans","Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol","Lucida Grande",Helvetica,Arial,sans-serif;white-space:pre-line"><br></span></div><div><font face="-apple-system, system-ui, BlinkMacSystemFont, Segoe UI, Roboto, Helvetica Neue, Fira Sans, Ubuntu, Oxygen, Oxygen Sans, Cantarell, Droid Sans, Apple Color Emoji, Segoe UI Emoji, Segoe UI Symbol, Lucida Grande, Helvetica, Arial, sans-serif"><span style="color:rgba(0,0,0,0.901961);white-space:pre-line"><br></span></font><div><br></div></div></div></div></div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Jun 7, 2020 at 5:27 PM Manuel Gómez <<a href="mailto:targen@gmail.com">targen@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">On Sun, Jun 7, 2020 at 5:44 PM Ben Franksen <<a href="mailto:ben.franksen@online.de" target="_blank">ben.franksen@online.de</a>> wrote:<br>
> That said, he did write in one of his EWDs that beginners(!) should be<br>
> tought programming with a language that does /not/ have an<br>
> implementation available, in order to enourage thinking denotationally<br>
> about programs rather than operationally, right from the start. The<br>
> reason he preferred an imperative language for such a beginner's course<br>
> (and also for communicating algorithms) is that recursion has a more<br>
> complicated semantics (in terms of weakest preconditions) than his 'do'<br>
> loop construct. This is important if, like Dijkstra did, you introduce<br>
> every language construct by formally stating its denotational semantics,<br>
> playing down the operational aspect as much as possible.<br>
<br>
As a fun anecdote, Dijkstra's language referred to here, the Guarded<br>
Command Language, has actually seen several implementations despite<br>
his explicit intent for implementations never to exist:<br>
<br>
<a href="https://metacpan.org/pod/Commands::Guarded" rel="noreferrer" target="_blank">https://metacpan.org/pod/Commands::Guarded</a><br>
<a href="https://web.archive.org/web/20091214010836/http://www.dc.fi.udc.es/ai/~cabalar/gcl/" rel="noreferrer" target="_blank">https://web.archive.org/web/20091214010836/http://www.dc.fi.udc.es/ai/~cabalar/gcl/</a><br>
<a href="https://web.archive.org/web/20080622163307/http://gacela.labf.usb.ve/GacelaWiki/" rel="noreferrer" target="_blank">https://web.archive.org/web/20080622163307/http://gacela.labf.usb.ve/GacelaWiki/</a><br>
<br>
The last one there was actually used in the university I went to as<br>
the language for the first programming course for incoming CS students<br>
for the better part of a decade, until the department switched those<br>
courses to Python.<br>
<br>
Of note, also, is that 12 years passed from EWD1036 to his letter on<br>
using Haskell to teach introductory programming.  I wonder if he ever<br>
wrote or shared his thoughts on whether this was merely a pragmatist's<br>
compromise, or a change of heart in light of Haskell's progress over<br>
those years: why did he not stick to GCL?<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div>David Duke</div><div>Professor of Computer Science</div><div>School of Computing University of Leeds UK</div><div><a href="mailto:E%3Aduke.j.david@gmail.com" target="_blank">E:duke.j.david@gmail.com</a></div><div>W:<a href="https://engineering.leeds.ac.uk/staff/334/Professor_David_Duke" target="_blank">https://engineering.leeds.ac.uk/staff/334/Professor_David_Duke</a></div></div></div></div></div></div></div></div></div>