[Haskell-cafe] The Definition of Haskell

[Todd Wilson]

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 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/20171217/89e6732d/attachment.html>