<div dir="ltr">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.<div><br></div><div>--Todd</div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, Dec 18, 2017 at 1:42 AM Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div lang="EN-GB" link="blue" vlink="purple"><div class="m_3071930886100628040WordSection1">
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:36.0pt">
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.<u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
</div></div><div lang="EN-GB" link="blue" vlink="purple"><div class="m_3071930886100628040WordSection1"><p class="MsoNormal"><span style="font-size:12.0pt">Yes – and Core is indeed formalised quite carefully (by Richard Eisenberg).  See
<a href="https://ghc.haskell.org/trac/ghc/ticket/14572#comment:8" target="_blank">https://ghc.haskell.org/trac/ghc/ticket/14572#comment:8</a>
<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">Simon<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> Haskell-Cafe [mailto:<a href="mailto:haskell-cafe-bounces@haskell.org" target="_blank">haskell-cafe-bounces@haskell.org</a>]
<b>On Behalf Of </b>Todd Wilson<br>
<b>Sent:</b> 17 December 2017 19:53<br>
<b>To:</b> Haskell Cafe <<a href="mailto:haskell-cafe@haskell.org" target="_blank">haskell-cafe@haskell.org</a>><br>
<b>Subject:</b> Re: [Haskell-cafe] The Definition of Haskell<u></u><u></u></span></p>
</div>
</div></div></div></div><div lang="EN-GB" link="blue" vlink="purple"><div class="m_3071930886100628040WordSection1"><div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
On Sat, Dec 16, 2017 at 9:14 PM Brandon Allbery <<a href="mailto:allbery.b@gmail.com" target="_blank">allbery.b@gmail.com</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Dunno about safety results, but <a href="https://www.haskell.org/onlinereport/haskell2010/" target="_blank">https://www.haskell.org/onlinereport/haskell2010/</a> exists (next revision expected in 2020 iirc).<u></u><u></u></p>
</div>
</blockquote>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
On Sat, Dec 16, 2017 at 9:22 PM Baojun Wang <<a href="mailto:wangbj@gmail.com" target="_blank">wangbj@gmail.com</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
SPJ may answered part of it in his talk Escape from the ivory tower: <a href="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" target="_blank">https://www.youtube.com/watch?v=re96UgMk6GQ&feature=share</a> from
 about 29 minutes.<u></u><u></u></p>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
</div>
</div>
</div></div></div></blockquote></div>