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