[ANN] patat - Terminal based presentation tool built with Pandoc

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
23 messages Options
12
Reply | Threaded
Open this post in threaded view
|

[ANN] patat - Terminal based presentation tool built with Pandoc

Jasper Van der Jeugt-2
I'm happy to announce `patat` (Presentations Atop The ANSI Terminal),
a small tool that allows you to show presentations using only an ANSI
terminal.

The main features are:

- Leverages the great Pandoc library to support many input formats
including Literate Haskell.
- Supports smart slide splitting.
- There is a live reload mode.
- Theming support.
- Optionally re-wrapping text to terminal width with proper indentation.
- Written in Haskell.

You can find more information here:

    https://github.com/jaspervdj/patat/blob/master/README.md

Peace,
Jasper
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: [ANN] patat - Terminal based presentation tool built with Pandoc

Luke Murphy
Jasper, it's great.

I am just writing a presentation with it now and saw this drop into my
inbox.

Nice job!

Luke


On 14.10.2016 11:33, Jasper Van der Jeugt wrote:

> I'm happy to announce `patat` (Presentations Atop The ANSI Terminal),
> a small tool that allows you to show presentations using only an ANSI
> terminal.
>
> The main features are:
>
> - Leverages the great Pandoc library to support many input formats
> including Literate Haskell.
> - Supports smart slide splitting.
> - There is a live reload mode.
> - Theming support.
> - Optionally re-wrapping text to terminal width with proper indentation.
> - Written in Haskell.
>
> You can find more information here:
>
>      https://github.com/jaspervdj/patat/blob/master/README.md
>
> Peace,
> Jasper
> _______________________________________________
> 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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: [ANN] patat - Terminal based presentation tool built with Pandoc

migmit-2
Wow. Just wow.

On Fri, Oct 14, 2016 at 11:37 AM, Luke Murphy <[hidden email]> wrote:
Jasper, it's great.

I am just writing a presentation with it now and saw this drop into my inbox.

Nice job!

Luke



On <a href="tel:14.10.2016" value="+3614102016" target="_blank">14.10.2016 11:33, Jasper Van der Jeugt wrote:
I'm happy to announce `patat` (Presentations Atop The ANSI Terminal),
a small tool that allows you to show presentations using only an ANSI
terminal.

The main features are:

- Leverages the great Pandoc library to support many input formats
including Literate Haskell.
- Supports smart slide splitting.
- There is a live reload mode.
- Theming support.
- Optionally re-wrapping text to terminal width with proper indentation.
- Written in Haskell.

You can find more information here:

     https://github.com/jaspervdj/patat/blob/master/README.md

Peace,
Jasper
_______________________________________________
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.

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


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: [ANN] patat - Terminal based presentation tool built with Pandoc

Guillaume Bouchard
Nice work,

The documentation state about "image" and "math" in the "style"
section. Is there a way to display math and images in this tool ?

On Fri, Oct 14, 2016 at 11:41 AM, Miguel <[hidden email]> wrote:

> Wow. Just wow.
>
> On Fri, Oct 14, 2016 at 11:37 AM, Luke Murphy <[hidden email]> wrote:
>>
>> Jasper, it's great.
>>
>> I am just writing a presentation with it now and saw this drop into my
>> inbox.
>>
>> Nice job!
>>
>> Luke
>>
>>
>>
>> On 14.10.2016 11:33, Jasper Van der Jeugt wrote:
>>>
>>> I'm happy to announce `patat` (Presentations Atop The ANSI Terminal),
>>> a small tool that allows you to show presentations using only an ANSI
>>> terminal.
>>>
>>> The main features are:
>>>
>>> - Leverages the great Pandoc library to support many input formats
>>> including Literate Haskell.
>>> - Supports smart slide splitting.
>>> - There is a live reload mode.
>>> - Theming support.
>>> - Optionally re-wrapping text to terminal width with proper indentation.
>>> - Written in Haskell.
>>>
>>> You can find more information here:
>>>
>>>      https://github.com/jaspervdj/patat/blob/master/README.md
>>>
>>> Peace,
>>> Jasper
>>> _______________________________________________
>>> 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.
>>
>>
>> _______________________________________________
>> 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.
>
>
>
> _______________________________________________
> 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.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: [ANN] patat - Terminal based presentation tool built with Pandoc

Jasper Van der Jeugt-2
Not really.  Math is displayed as the math's source, and for images it
displays the URL.  The settings impact only the style in which these
strings are printed.

There is an idea floating around to support images in iTerm2 [1], or
we could support low-res ones in 256-color terminals, but it's still
debatable if this is a good idea.

[1]: https://github.com/jaspervdj/patat/issues/6

Peace,
Jasper

On Fri, Oct 14, 2016 at 1:00 PM, Guillaume Bouchard
<[hidden email]> wrote:

> Nice work,
>
> The documentation state about "image" and "math" in the "style"
> section. Is there a way to display math and images in this tool ?
>
> On Fri, Oct 14, 2016 at 11:41 AM, Miguel <[hidden email]> wrote:
>> Wow. Just wow.
>>
>> On Fri, Oct 14, 2016 at 11:37 AM, Luke Murphy <[hidden email]> wrote:
>>>
>>> Jasper, it's great.
>>>
>>> I am just writing a presentation with it now and saw this drop into my
>>> inbox.
>>>
>>> Nice job!
>>>
>>> Luke
>>>
>>>
>>>
>>> On 14.10.2016 11:33, Jasper Van der Jeugt wrote:
>>>>
>>>> I'm happy to announce `patat` (Presentations Atop The ANSI Terminal),
>>>> a small tool that allows you to show presentations using only an ANSI
>>>> terminal.
>>>>
>>>> The main features are:
>>>>
>>>> - Leverages the great Pandoc library to support many input formats
>>>> including Literate Haskell.
>>>> - Supports smart slide splitting.
>>>> - There is a live reload mode.
>>>> - Theming support.
>>>> - Optionally re-wrapping text to terminal width with proper indentation.
>>>> - Written in Haskell.
>>>>
>>>> You can find more information here:
>>>>
>>>>      https://github.com/jaspervdj/patat/blob/master/README.md
>>>>
>>>> Peace,
>>>> Jasper
>>>> _______________________________________________
>>>> 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.
>>>
>>>
>>> _______________________________________________
>>> 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.
>>
>>
>>
>> _______________________________________________
>> 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.
> _______________________________________________
> 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.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: [ANN] patat - Terminal based presentation tool built with Pandoc

Brandon Allbery
On Fri, Oct 14, 2016 at 8:23 AM, Jasper Van der Jeugt <[hidden email]> wrote:
There is an idea floating around to support images in iTerm2 [1], or
we could support low-res ones in 256-color terminals, but it's still
debatable if this is a good idea.

You can render images directly into any X11 terminal which supports $WINDOWID, which is most of them.

--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

A backhanded compliment and a dilemma

Richard A. O'Keefe
In reply to this post by Jasper Van der Jeugt-2
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.
Reply | Threaded
Open this post in threaded view
|

Re: A backhanded compliment and a dilemma

Rahul Muttineni
You core problem has existed since 1994 :) It'd a bit disappointing that we've only made so much progress in the psychological perspective in 26 years.

Quoting [1], a study on prototyping software with different languages:

One observer described the solution as “cute but not extensible” (para-phrasing); this comment slipped its way into an initial draft of the final report, which described the Haskell prototype as being “too cute for its own good” (the phrase was later removed after objection by the first author of this paper).
We mention these responses because they must be anticipated in the future. If functional languages are to become more widely used, various sociological and psychological barriers must be overcome. As a community we should be aware of these barriers and realize that they will not disappear overnight.

People only like solutions when they have a deep problem needing to be solved. Giving Haskell to people who are already happy with the status quo will not turn any heads. Think about the deep problem that can solved by machine-checked specifications and who would be interested. Sorry for the vague answer, but it's the best I can give right now.

Hope that helps,

Rahul

[1] http://www.cse.iitk.ac.in/users/karkare/courses/2010/cs653/Papers/hudak_haskell_sw_prototype.pdf
    (Thanks to John Hughes for informing us of this paper at FunctionalConf 2016.)

On Thu, Oct 20, 2016 at 6:27 AM, Richard A. O'Keefe <[hidden email]> 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.



--
Rahul Muttineni

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: A backhanded compliment and a dilemma

Tobias Dammers

Consider this: the most popular programming languages overall are (arguably) PHP and Java, despite being almost half a century behind the state of the art of programming language design in many ways. Ask yourself why that is (and no, I haven't fully figured this one out myself either).


On Oct 20, 2016 5:22 AM, "Rahul Muttineni" <[hidden email]> wrote:
You core problem has existed since 1994 :) It'd a bit disappointing that we've only made so much progress in the psychological perspective in 26 years.

Quoting [1], a study on prototyping software with different languages:

One observer described the solution as “cute but not extensible” (para-phrasing); this comment slipped its way into an initial draft of the final report, which described the Haskell prototype as being “too cute for its own good” (the phrase was later removed after objection by the first author of this paper).
We mention these responses because they must be anticipated in the future. If functional languages are to become more widely used, various sociological and psychological barriers must be overcome. As a community we should be aware of these barriers and realize that they will not disappear overnight.

People only like solutions when they have a deep problem needing to be solved. Giving Haskell to people who are already happy with the status quo will not turn any heads. Think about the deep problem that can solved by machine-checked specifications and who would be interested. Sorry for the vague answer, but it's the best I can give right now.

Hope that helps,

Rahul

[1] http://www.cse.iitk.ac.in/users/karkare/courses/2010/cs653/Papers/hudak_haskell_sw_prototype.pdf
    (Thanks to John Hughes for informing us of this paper at FunctionalConf 2016.)

On Thu, Oct 20, 2016 at 6:27 AM, Richard A. O'Keefe <[hidden email]> 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.



--
Rahul Muttineni

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

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: A backhanded compliment and a dilemma

M Farkas-Dyck-2
On 19/10/2016, Tobias Dammers <[hidden email]> wrote:
> Consider this: the most popular programming languages overall are
> (arguably) PHP and Java, despite being almost half a century behind the
> state of the art of programming language design in many ways. Ask yourself
> why that is (and no, I haven't fully figured this one out myself either).

Some people like to be tied up and whipped; i think it's the same phenomenon.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: A backhanded compliment and a dilemma

Tobias Dammers

All joking aside, I'm afraid we must face the reality that the kind of programmer who is willing to go through great lengths to get reasonably correct and maintainable code is the exception, not the norm. Even in fields where extreme levels of certainty and confidence are required (think avionics, medical devices, nuclear installation, weapons), the preferred strategy still seems to be rigid processes and lots of manual labor. Obviously events like the Ariane 5 incidents aren't helpful there.


On Oct 20, 2016 8:30 AM, "M Farkas-Dyck" <[hidden email]> wrote:
On 19/10/2016, Tobias Dammers <[hidden email]> wrote:
> Consider this: the most popular programming languages overall are
> (arguably) PHP and Java, despite being almost half a century behind the
> state of the art of programming language design in many ways. Ask yourself
> why that is (and no, I haven't fully figured this one out myself either).

Some people like to be tied up and whipped; i think it's the same phenomenon.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: A backhanded compliment and a dilemma

Simon  Thompson
In reply to this post by Richard A. O'Keefe
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 <[hidden email]> 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
[hidden email] | 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.
Reply | Threaded
Open this post in threaded view
|

Re: A backhanded compliment and a dilemma

Imants Cekusins
In reply to this post by Tobias Dammers
> the kind of programmer who is willing to ...

People choosing language / framework may not be the same people who write code. People who begin coding a project may not be the same people who complete and maintain it.

All these groups (choose, begin, complete, maintain) may develop different preferences for languages / frameworks. However the 'choose' group will affect language usage stats more than the other groups.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: A backhanded compliment and a dilemma

Tobias Dammers

Very true, however, the "choose" group has to take the rest of the chain into account. The fact that certain types if programmers gravitate towards certain technologies, and the reality of a limited hiring pool and a high demand, means that programmers' tech preferences ARE an important factor, even when plenty of programmers work with a stack they wouldn't necessarily pick themselves.


On Oct 20, 2016 8:54 AM, "Imants Cekusins" <[hidden email]> wrote:
> the kind of programmer who is willing to ...

People choosing language / framework may not be the same people who write code. People who begin coding a project may not be the same people who complete and maintain it.

All these groups (choose, begin, complete, maintain) may develop different preferences for languages / frameworks. However the 'choose' group will affect language usage stats more than the other groups.

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

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: A backhanded compliment and a dilemma

Imants Cekusins
 the "choose" group has to take the rest of the chain into account

Choosers rarely consult and listen to the other groups even when those other groups are present and voice their preferences. Job ads where employer is open to suggestions about the language are not common.

Preferences may differ. The same person may prefer different language depending on which group they are in.

If the same group and people within that group did all the stages: choose, begin, complete, maintain, they'd make a more balanced decision.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: A backhanded compliment and a dilemma

Jon Fairbairn
In reply to this post by Richard A. O'Keefe
"Richard A. O'Keefe" <[hidden email]> writes:

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

Just a shot in the dark: would it help to put all the braces and
semicolons in explicitly? :-)


--
Jón Fairbairn                                 [hidden email]

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: A backhanded compliment and a dilemma

Jeremy O'Donoghue
In reply to this post by Richard A. O'Keefe
I suspect that there are few on this list who actually participate in significant standards bodies, so it is perhaps understandable that the replies so far tend towards "everyone uses language $FOO even though it sucks" and "people who choose the implementation language for a standard don't code it".

I participate in standards development across multiple bodies, and (at least arguably) in an area where formal methods would be particularly helpful: standards focussed around device security. I hope my perspective will help.

The first thing to understand is that most standards bodies have participation from a wide range of individuals and organisations. There is no standardised recruiting process or essential body of knowledge, although in practice the contributors to most standards at the working group level have a generally acknowledged level of expertise in the subject under standardisation.

A huge part of the expectation of a member of a working group is that they are competent to review and comment intelligently on proposed changes and additions to the standard in question. This implies that the working group needs to use language (in the widest sense) that is accessible to all of its members. To be specific to my own standards participation, I work on a set of standards around the "Trusted Execution Environment". This is essentially a small security-oriented runtime designed to support cryptographic operations. It offers a standard API to developers of applications which use the environment.

The system is described mainly in terms of the behaviour of its APIs, along with normative English language text describing those things that are not straightforwardly expressed by a function signature - I think this is a fairly common approach in standardisation, and as stated, essentially relies for its correctness on heroic efforts of checking text. The fact that we occasionally find "obvious" errors in text written some years ago is a testament to the fact that this process doesn't work very well, and I would suggest that thesis actually well understood in the standards world.

However, and I say this with sadness, the availability of tooling to adequately support the development of machine checked specifications by traditional standards bodies is just not there. IN the case of the Trusted Execution Environment, which is one I know, the closest equivalent for which I am aware of a formal proof is SEL4 (you could certainly build a Trusted Execution Environment on top of SEL4, for example).

Here's the problem: I am, I believe, a rare example of someone who knows (some) Haskell - hobbyist for over 10 years - and understand the implementation domain of TEE well. Frankly, the SEL4 proofs are beyond my ability to understand, and that means that it is beyond my ability to determine whether they really represent an adequate formal proof of the correctness of SEL4 (other than the fact that I know who did the work, of course, and as such I actually do trust it).

I would posit that there is no-one else in the groups within which I work who has any more than superficial knowledge or understanding of Haskell, proof assistants and other important concepts. In effect, this means that the expert group within which I work would be unlikely to be competent to create a machine checked specification because even if, say, I were to do so, others would be unable to review this. Since it seems unlikely (even if it were desirable) that standards bodies work will be performed only by people with a PhD in type theory, the reality is that the mechanisms that exist today are inaccessible to us.

Now, I want to be clear that I believe that the work done by e.g. the SEL4 team and others is hugely important in getting us to a place where this situation will change, since we are gradually building a set of "baseline" proofs around common behaviours, but it is important to consider that:
  • The proofs themselves contain little documentation to explain how they fit together, which makes them very inaccessible for those wishing to learn from or reuse them. The linked proof is for operation of the ARM architecture TCB - this is something I understand quite well in "everyday life" terms, but it is completely opaque to me as a proof.
  • The sub-proofs are not structured in a way which fosters reuse. There are multiple proof tools, each with their own quirks and language, and for which it appears that porting proofs between them is tricky.
  • Proof tools themselves are not user friendly.
  • The proofs are too far divorced from real implementation to make them helpful to implementers (who are usually the end customers of a specification).
For what it's worth, some of us (like myself) do create our own Haskell/Ocaml/whatever models of behaviour for proposed new features, but we use these to inform our checking process, rather than as input to the standards process.

In practice, many standards bodies are addressing the inadequacies of the "hand crafted, hand checked" specification model by attempting to create (usually Open Source) reference implementations that serve as a normative specification of system behaviour. For a number of reasons, I am not convinced that this will be much more successful than the current approach, but I do believe that it is indicative that the standards field is aware of the issues it faces with increasingly complex specifications, and is looking for solutions.

The challenge for the academic community is to demonstrate that there is a better way which is reasonably accessible to practitioners. I would suggest that a fairly good starting point of practical use (as opposed to academic interest) is a well documented machine checked specification for the C programming language with reasonably user-friendly tools to accompany it (this part could be the commercial spin-off), as this is, in practice, what many programming languages and API specifications are built upon - at least until Rust proves itself comprehensively superior for the task.

Best regards
Jeremy


On 20 October 2016 at 01:57, Richard A. O'Keefe <[hidden email]> 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.


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: A backhanded compliment and a dilemma

Andrey Chudnov
In reply to this post by Simon Thompson
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 <[hidden email]> 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
> [hidden email] | 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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: A backhanded compliment and a dilemma

Joachim Durchholz
In reply to this post by M Farkas-Dyck-2
Am 20.10.2016 um 08:30 schrieb M Farkas-Dyck:
> On 19/10/2016, Tobias Dammers <[hidden email]> wrote:
>> Consider this: the most popular programming languages overall are
>> (arguably) PHP and Java, despite being almost half a century behind the
>> state of the art of programming language design in many ways. Ask yourself
>> why that is (and no, I haven't fully figured this one out myself either).
>
> Some people like to be tied up and whipped; i think it's the same phenomenon.

That is neither funny nor accurate.

Not funny for those among us who happen to program in one of these
languages, for whatever reason.

And wildly inaccurable because while Haskell is an excellent language,
the same cannot be said about several relevant parts of its ecosystem.

In fact from the perspective of a Java programmer, mentions of "Cabal
hell" sounds just like "some people like being tortured", which
obviously isn't true either.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: A backhanded compliment and a dilemma

Joachim Durchholz
In reply to this post by Imants Cekusins
Am 20.10.2016 um 09:32 schrieb Imants Cekusins:
>>  the "choose" group has to take the rest of the chain into account
>
> Choosers rarely consult and listen to the other groups even when those
> other groups are present and voice their preferences.

They consult with their architects if they have no personal expertise.
If they have personal expertise, they usually *are* the architects.

Architects tend to stick with established technology because switching
is costly (loss of productivity because programmers have to relearn,
loss of codebase that's incompatible with the new ecosystem, loss of
tool integration that needs to be prepared for the new ecosystem, loss
of programmer time who need to rewrite stuff), *plus* it is risky
because nobody can guarantee that you will ever recoup the losses, let
alone gain an edge.

Just do the math: assuming a developer-year costs USD 100,000 (not too
absurd in Western countries though there are obviously differences), a
team of ten developers working for a year to embark on a new language is
a full million dollars that needs to amortize.
And you need to guarantee that the transition is done after a year, and
that programmers will be more productive by 50%, and then it is still
three years until that expense is amortized.
You simply don't do that. You cannot (or at least should not) bet your
company's existence on that kind of stuff, particularly if those
guarantees are not available.
In practice, drastic coding infrastructure changes tend to take decades.
Large businesses (i.e. those who have the money to actually experiment
with disruptive stuff) are currently in the process of migrating their
applications from mainframes to webservices, and the typical timescale
for that is in years, sometimes decades, even for them.

Things change if you get a guarantee. If a competitor is able to make
their business processes substantially more flexible, then there you
have your guarantee, and then you'll find the employers who are willing
to use^Wtry that disruptive technology.
Webservices and enterprise buses were such changes, for example - and
they are still migrating.

 > Job ads where
> employer is open to suggestions about the language are not common.

Well, changing the language in a running business process is a
high-risk, dubious-reward proposition.
You will have a hard time convincing anybody of trying that out.

> If the same group and people within that group did all the stages:
> choose, begin, complete, maintain, they'd make a more balanced decision.

Talking as somebody who has seen both sides of the fence, I can say that
these decisions cannot be made "more balanced".
You have to balance risk against reward, all while taking constraints
like developer availability, in-house ability to actually make use of
the advantages, retraining costs and overall profitability into account.

Going just by qualities of the language would be the unbalanced
decision, I'd say.
_______________________________________________
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.
12