[Haskell-cafe] The Definition of Haskell

[Todd Wilson]

Thanks, all, this was indeed what I was looking for, with the reference to
Ott as an added bonus. It looks like formalizing and proving safety for
this system in a proof assistant would make a good project.

--Todd

On Mon, Dec 18, 2017 at 1:42 AM Simon Peyton Jones <simonpj at microsoft.com>
wrote:

> I see SPJ's point, but he makes another point in the same video, which is
> that Haskell has a small, internal core language to which everything must
> elaborate, so this would seem to make formalization even more attractive:
> formalize and prove safety for the core language once and for all, and then
> specify the elaborations and check their properties modularly, which should
> work well even in the face of language evolution.
>
>
>
> Yes – and Core is indeed formalised quite carefully (by Richard
> Eisenberg).  See https://ghc.haskell.org/trac/ghc/ticket/14572#comment:8
>
>
>
> Simon
>
>
>
> *From:* Haskell-Cafe [mailto:haskell-cafe-bounces at haskell.org] *On Behalf
> Of *Todd Wilson
> *Sent:* 17 December 2017 19:53
> *To:* Haskell Cafe <haskell-cafe at haskell.org>
> *Subject:* Re: [Haskell-cafe] The Definition of Haskell
>
>
>
> On Sat, Dec 16, 2017 at 9:14 PM Brandon Allbery <allbery.b at gmail.com>
> wrote:
>
> Dunno about safety results, but
> https://www.haskell.org/onlinereport/haskell2010/ exists (next revision
> expected in 2020 iirc).
>
>
>
> Although this can be considered a definition of the language, it is by no
> means a formal definition of the static and dynamic semantics of the
> language in a form amenable to representation in systems like Coq, where
> metatheory might be checked.
>
>
>
> On Sat, Dec 16, 2017 at 9:22 PM Baojun Wang <wangbj at gmail.com> wrote:
>
> SPJ may answered part of it in his talk Escape from the ivory tower:
> https://www.youtube.com/watch?v=re96UgMk6GQ&feature=share
> <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.youtube.com%2Fwatch%3Fv%3Dre96UgMk6GQ%26feature%3Dshare&data=02%7C01%7Csimonpj%40microsoft.com%7C6fb497b3f6c94c81876e08d545882101%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636491373335007410&sdata=5WnVwESDGAotRmeUq6wevSmwgsg6hFFGe6c90YYFv6E%3D&reserved=0> from
> about 29 minutes.
>
>
>
> Nice talk; thanks for the reference. To summarize: formalization, which is
> a lot of work, leads to standardization and the reluctance to change the
> language, and one of Haskell's strong points is that it is constantly
> evolving.
>
>
>
> I see SPJ's point, but he makes another point in the same video, which is
> that Haskell has a small, internal core language to which everything must
> elaborate, so this would seem to make formalization even more attractive:
> formalize and prove safety for the core language once and for all, and then
> specify the elaborations and check their properties modularly, which should
> work well even in the face of language evolution.
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20171218/17750796/attachment.html>