<div dir="ltr">Right, sure. I&#39;d still argue that if you are worried about trust, then between<div>the Agda type checker, the Agda to Haskell compiler, the Haskell compiler,</div><div>and the implementation of Haskell Integer arithmetic, I trust the Integer</div><div>arithmetic the most, by several orders of magnitude.</div><div><br></div><div>If you want to experiment with this approach, however, you can implement<br></div><div>macro digits using the normal Agda natural numbers for now and swap them</div><div>out later if (when?) we add builtin machine integers.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Sep 21, 2016 at 3:26 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"><span class="">On Wed, 2016-09-21 at 14:34 +0200, Ulf Norell wrote:<br>
&gt; How is this better than what we do at the moment? It seems to me that<br>
&gt; your postulated properties of the macro digit operations are going to<br>
&gt; be more complicated than what we postulate right now (namely that<br>
&gt; Haskell Integer arithmetic implement the expected functions on natural<br>
&gt; numbers).<br>
&gt;<br>
<br>
</span>I do not understand this argument. Let me describe some details.<br>
<br>
I expect that a macrodigit is about a half of a  machine word.<br>
For example, for a 64 bit machine, a macrodigit is (probably) 31 bit,<br>
and it is represented as  Int  (small integer) in Haskell<br>
(something of this sort, I do not know details).<br>
And  Integer  is probably represented in GHC implementation as a list<br>
(array?) of macrodigits.<br>
<br>
Currently the Agda library postulates certain properties of complex<br>
arithmetical programs in GHC, written (probably) in C, that process<br>
lists (arrays?) of macrodigits.<br>
Right?<br>
<br>
And I suggest for Agda: to postulte only the properties of a few<br>
operations on Macrodigit. For example:<br>
_+m_ is commutative on Integer/M  (Integer modulo M), where M = 2^31.<br>
And _+m_ is done by a hardware, by a single processor instruction, it<br>
has not any program structure, in any language. So it cannot be<br>
subjected to a proof.<br>
So, postulated are only a few properties of a few hardware operations.<br>
And all the complex C programs for arithmetic on Integer to be replaced<br>
with Agda programs (in Agda library) processing lists of macrodigits,<br>
and also being accompanied with proofs.<br>
<br>
So, a larger part is made explicit for Agda and proved, and a smaller<br>
part remains postulated.<br>
<br>
?<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
&gt;<br>
&gt;<br>
&gt; On Wed, Sep 21, 2016 at 2:20 PM, Sergei Meshveliani &lt;<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>&gt;<br>
&gt; wrote:<br>
&gt;         On Wed, 2016-09-21 at 12:52 +0200, Ulf Norell wrote:<br>
&gt;         &gt;<br>
&gt;         &gt; On Wed, Sep 21, 2016 at 11:51 AM, Sergei Meshveliani<br>
&gt;         &gt; &lt;<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>&gt; wrote:<br>
&gt;         &gt;         Ulf Norell wrote recently<br>
&gt;         &gt;<br>
&gt;         &gt;         &gt; [..]<br>
&gt;         &gt;         &gt; natural number operations (_+_, _*_ etc) are<br>
&gt;         compiled to the<br>
&gt;         &gt;         &gt; corresponding Haskell Integer operations.<br>
&gt;         &gt;<br>
&gt;         &gt;         But this means that the properties of these<br>
&gt;         operations on Nat<br>
&gt;         &gt;         become postulated.<br>
&gt;         &gt;         Do they?<br>
&gt;         &gt;<br>
&gt;         &gt;         For example, the commutativity property  +-comm  of<br>
&gt;         &gt;         Data.Nat.Properties.Simple<br>
&gt;         &gt;         is proved in this module for Nat represented in<br>
&gt;         unary system<br>
&gt;         &gt;         and for the algorithm for _+_<br>
&gt;         &gt;         given in Data.Nat.<br>
&gt;         &gt;         Now as _+_ is compiled to  +-via-Haskell-Integer,<br>
&gt;         the proof<br>
&gt;         &gt;         for +-comm  is not a proof for<br>
&gt;         &gt;         +-via-Haskell-Integer.<br>
&gt;         &gt;<br>
&gt;         &gt;         Can somebody explain, please?<br>
&gt;         &gt;<br>
&gt;         &gt;<br>
&gt;         &gt; Operationally, the proof of +-comm carries no bits of<br>
&gt;         information, and<br>
&gt;         &gt; so can be erased at runtime.<br>
&gt;         &gt;<br>
&gt;         &gt;<br>
&gt;         &gt; If you&#39;re concerned about correctness, there is indeed an<br>
&gt;         implicit<br>
&gt;         &gt; assumption that the Haskell<br>
&gt;         &gt; Integer arithmetic functions are semantically equivalent to<br>
&gt;         the unary<br>
&gt;         &gt; natural number functions<br>
&gt;         &gt; defined in Agda (and so that the proof of +comm for unary<br>
&gt;         numbers<br>
&gt;         &gt; implies +comm for Haskell<br>
&gt;         &gt; Integers). I feel pretty confident that this is the case.<br>
&gt;         Certainly<br>
&gt;         &gt; more confident than I am in there<br>
&gt;         &gt; being no inconsistency bugs in the type checker, for<br>
&gt;         instance.<br>
&gt;         &gt;<br>
&gt;<br>
&gt;<br>
&gt;         Being not able to provably verify the type checker<br>
&gt;         (and also MAlonzo, GHC, linker, and hardware) does not mean<br>
&gt;         that one<br>
&gt;         needs to assume/postulate the properties of all the upper<br>
&gt;         levels. The<br>
&gt;         more levels are verified the better<br>
&gt;<br>
&gt;         (by the way, one can imagine a provably verified type checker,<br>
&gt;         provably<br>
&gt;         verified Agda interpreter ... -- may such have sense?).<br>
&gt;<br>
&gt;         Adding proofs to efficient programs for a generic fraction<br>
&gt;         arithmetic,<br>
&gt;         polynomial arithmetic, etc, allows it to preserve performance.<br>
&gt;         As to natural numbers, the provable part can cover without<br>
&gt;         performance<br>
&gt;         loss everything besides macrodigits.<br>
&gt;<br>
&gt;         Namely, suppose that we represent Natural as  Nat&#39; = List<br>
&gt;         Macrodigit,<br>
&gt;         map Macrodigit to Int of Haskell and make arithmetic<br>
&gt;         operations on<br>
&gt;         Macrodigits built-in, postulate several properties of the<br>
&gt;         Macrodidit<br>
&gt;         arithmetic, program in Agda arithmetical operations on Nat&#39; by<br>
&gt;         processing lists of macrodigits, add the proofs for the<br>
&gt;         properties (like<br>
&gt;         say +-comm) for Nat&#39;.<br>
&gt;         With this approach the arithmetic in Nat  a) will be fast<br>
&gt;         enough,<br>
&gt;         b) the postulated part will be restricted to operations on<br>
&gt;         Macrodigit,<br>
&gt;         so that the programs will be more verified.<br>
&gt;<br>
&gt;         Has this approach sense?<br>
&gt;<br>
&gt;         Regards,<br>
&gt;<br>
&gt;         ------<br>
&gt;         Sergei<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt;<br>
<br>
<br>
</div></div></blockquote></div><br></div>