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@gmail.com> wrote:

On Sun, Jun 7, 2020 at 5:44 PM Ben Franksen <ben.franksen@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.