[Haskell-cafe] A backhanded compliment and a dilemma

[Andrey Chudnov]

Simon, with JSCert it's proofs in Coq --- not quick-checked Haskell 
code. The level of assurance is different.

Richard, if not a secret, which conference did you send it to? I think 
that a PL conference would find a paper on this topic interesting and 
readable, as long as it's well motivated and there are substantial 
findings/contributions. So, something like PLDI would be a good fit. 
Depending on the degree of contribution, POPL and ICFP might be other 
options. I don't know if publishing there would help your effort in 
enlightening the writers of standards for more widely used languages, 
though.

/Andrey


On 10/20/2016 02:49 AM, Simon Thompson wrote:
> 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
>
> _______________________________________________
> 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.