<div dir="ltr">How is this better than what we do at the moment? It seems to me that<br><div>your postulated properties of the macro digit operations are going to be more</div><div>complicated than what we postulate right now (namely that Haskell Integer</div><div>arithmetic implement the expected functions on natural numbers).</div><div><br></div><div>/ Ulf<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Sep 21, 2016 at 2:20 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5">On Wed, 2016-09-21 at 12:52 +0200, Ulf Norell wrote:<br>
&gt;<br>
&gt; On Wed, Sep 21, 2016 at 11:51 AM, Sergei Meshveliani<br>
&gt; &lt;<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>&gt; wrote:<br>
&gt;         Ulf Norell wrote recently<br>
&gt;<br>
&gt;         &gt; [..]<br>
&gt;         &gt; natural number operations (_+_, _*_ etc) are compiled to the<br>
&gt;         &gt; corresponding Haskell Integer operations.<br>
&gt;<br>
&gt;         But this means that the properties of these operations on Nat<br>
&gt;         become postulated.<br>
&gt;         Do they?<br>
&gt;<br>
&gt;         For example, the commutativity property  +-comm  of<br>
&gt;         Data.Nat.Properties.Simple<br>
&gt;         is proved in this module for Nat represented in unary system<br>
&gt;         and for the algorithm for _+_<br>
&gt;         given in Data.Nat.<br>
&gt;         Now as _+_ is compiled to  +-via-Haskell-Integer,  the proof<br>
&gt;         for +-comm  is not a proof for<br>
&gt;         +-via-Haskell-Integer.<br>
&gt;<br>
&gt;         Can somebody explain, please?<br>
&gt;<br>
&gt;<br>
&gt; Operationally, the proof of +-comm carries no bits of information, and<br>
&gt; so can be erased at runtime.<br>
&gt;<br>
&gt;<br>
&gt; If you&#39;re concerned about correctness, there is indeed an implicit<br>
&gt; assumption that the Haskell<br>
&gt; Integer arithmetic functions are semantically equivalent to the unary<br>
&gt; natural number functions<br>
&gt; defined in Agda (and so that the proof of +comm for unary numbers<br>
&gt; implies +comm for Haskell<br>
&gt; Integers). I feel pretty confident that this is the case. Certainly<br>
&gt; more confident than I am in there<br>
&gt; being no inconsistency bugs in the type checker, for instance.<br>
&gt;<br>
<br>
</div></div>Being not able to provably verify the type checker<br>
(and also MAlonzo, GHC, linker, and hardware) does not mean that one<br>
needs to assume/postulate the properties of all the upper levels. The<br>
more levels are verified the better<br>
<br>
(by the way, one can imagine a provably verified type checker, provably<br>
verified Agda interpreter ... -- may such have sense?).<br>
<br>
Adding proofs to efficient programs for a generic fraction arithmetic,<br>
polynomial arithmetic, etc, allows it to preserve performance.<br>
As to natural numbers, the provable part can cover without performance<br>
loss everything besides macrodigits.<br>
<br>
Namely, suppose that we represent Natural as  Nat&#39; = List Macrodigit,<br>
map Macrodigit to Int of Haskell and make arithmetic operations on<br>
Macrodigits built-in, postulate several properties of the Macrodidit<br>
arithmetic, program in Agda arithmetical operations on Nat&#39; by<br>
processing lists of macrodigits, add the proofs for the properties (like<br>
say +-comm) for Nat&#39;.<br>
With this approach the arithmetic in Nat  a) will be fast enough,<br>
b) the postulated part will be restricted to operations on Macrodigit,<br>
so that the programs will be more verified.<br>
<br>
Has this approach sense?<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
<br>
</blockquote></div><br></div>