[Haskell-cafe] A backhanded compliment and a dilemma

[Simon Thompson]

Hi Richard - are you aware of the work of Philippa Gardner and her colleagues on formalising ECMAScript?

  http://psvg.doc.ic.ac.uk/research/javascript.html

Exciting stuff! They’ve certainly had their work published.

Kind regards,

Simon


> On 20 Oct 2016, at 01:57, Richard A. O'Keefe <ok at cs.otago.ac.nz> wrote:
> 
> TL;DR - Haskell mistaken for pseudo-code, a case study on machine-
> checked specification for use in standards can't or won't be read
> by the people who need it (who aren't the people in this mailing list).
> 
> A couple of years ago, while trying to implement a programming language
> with >30 years of use and an actual ANSI standard, I encountered a gap
> in the standard where an aspect of arithmetic was referred to the
> Language Independent Arithmetic standard, which had in fact nothing
> whatsoever to say on the topic.  In consequence of this gap, existing
> implementations of this language implement that feature with different
> semantics.  Poking around, I found a smaller but similar hole in SQL,
> and similar issues in other languages.
> 
> There was no existing specification that any of these could refer to.
> So I set out to write one.  Having seen other problems in standards
> caused by definitions that had not been adequately proof-read,
> I decided that I wanted a specification that had
> - been type-checked
> - had been tested reasonably thoroughly
> 
> Since I'm writing in this mailing list, you can guess what I thought
> was a good way to do this: I wrote the specification in quite direct
> Haskell, putting effort into clarity at the expense of efficiency,
> and I used QuickCheck to test the specification.  I still don't know
> whether to be pleased that QuickCheck found mistakes -- demonstrating
> my point that specifications need to be checked thoroughly -- or
> ashamed that I'm still making such mistakes.
> 
> My problem:  I can't get this published.
> 
> The backhanded compliment:  the last reviewer excoriated me
> for having too much pseudocode in my paper.  (Despite the paper
> stating explicitly that ALL code in the paper was real code that
> had been executed.)  You got it:  Haskell doesn't look like a "real"
> programming language, but like something written for human
> comprehension during design.
> 
> The dilemma: what I want to do is to tell people working
> on standards that we NEED to have machine-checked specifications
> and that we HAVE the technology to write such specifications and
> test them (oh and by the way here's this specification I wrote to
> fill that gap).  But people who read Haskell well enough to read
> my specification don't need to be persuaded of this, and in all
> honesty, could write the specification for themselves if it
> occurred to them.  Yet the people who do need to be told that there
> is a much better way to write standards than say the ECMAScript way
> don't read Haskell, and won't be interested in learning to do so
> until they've been persuaded...
> 
> So where would _you_ send a case study on machine-checked specification?
> _______________________________________________
> 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.

Simon Thompson | Professor of Logic and Computation 
School of Computing | University of Kent | Canterbury, CT2 7NF, UK
s.j.thompson at kent.ac.uk | M +44 7986 085754 | W www.cs.kent.ac.uk/~sjt