Re: [Haskell-cafe] A backhanded compliment and a dilemma

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 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@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.