[Haskell-cafe] Looking for a paper [Dijkstra-Dot]

[David Duke]

Rather than denotationally, I'd emphasise the axiomatic foundations of GCL
in terms of wp.
Whilst EWD had plenty to say about programming languages his over
arching concern was programming methodology and the implementation
of correct programs wrt a specification.
It is not just a matter of simpler semantics.  In 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,
unfortunately no one had notes or could recall. The event was "Advanced
Course on Functional Programming and its Applications" 1981.Whilst I
believe on the basis of the EWD'staDijkstra thought highly of FP in
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
his
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:
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"
[Dijkstra "*To the members of the Budget Council" 12 April 2001.*

Indeed




On Sun, Jun 7, 2020 at 5:27 PM Manuel Gómez <targen at gmail.com> wrote:

> On Sun, Jun 7, 2020 at 5:44 PM Ben Franksen <ben.franksen at online.de>
> wrote:
> > That said, he did write in one of his EWDs that beginners(!) should be
> > tought programming with a language that does /not/ have an
> > implementation available, in order to enourage thinking denotationally
> > about programs rather than operationally, right from the start. The
> > reason he preferred an imperative language for such a beginner's course
> > (and also for communicating algorithms) is that recursion has a more
> > complicated semantics (in terms of weakest preconditions) than his 'do'
> > loop construct. This is important if, like Dijkstra did, you introduce
> > every language construct by formally stating its denotational semantics,
> > playing down the operational aspect as much as possible.
>
> As a fun anecdote, Dijkstra's language referred to here, the Guarded
> Command Language, has actually seen several implementations despite
> his explicit intent for implementations never to exist:
>
> https://metacpan.org/pod/Commands::Guarded
>
> https://web.archive.org/web/20091214010836/http://www.dc.fi.udc.es/ai/~cabalar/gcl/
>
> https://web.archive.org/web/20080622163307/http://gacela.labf.usb.ve/GacelaWiki/
>
> The last one there was actually used in the university I went to as
> the language for the first programming course for incoming CS students
> for the better part of a decade, until the department switched those
> courses to Python.
>
> Of note, also, is that 12 years passed from EWD1036 to his letter on
> using Haskell to teach introductory programming.  I wonder if he ever
> wrote or shared his thoughts on whether this was merely a pragmatist's
> compromise, or a change of heart in light of Haskell's progress over
> those years: why did he not stick to GCL?
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.



-- 
David Duke
Professor of Computer Science
School of Computing University of Leeds UK
E:duke.j.david at gmail.com
W:https://engineering.leeds.ac.uk/staff/334/Professor_David_Duke
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200607/7f613f37/attachment-0001.html>