<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"><<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"><div class="HOEnZb"><div class="h5">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 compiled to the<br>
> > corresponding Haskell Integer operations.<br>
><br>
> But this means that the properties of these 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 unary system<br>
> and for the algorithm for _+_<br>
> given in Data.Nat.<br>
> Now as _+_ is compiled to +-via-Haskell-Integer, 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 information, and<br>
> so can be erased at runtime.<br>
><br>
><br>
> If you're concerned about correctness, there is indeed an implicit<br>
> assumption that the Haskell<br>
> Integer arithmetic functions are semantically equivalent to the unary<br>
> natural number functions<br>
> defined in Agda (and so that the proof of +comm for unary numbers<br>
> implies +comm for Haskell<br>
> Integers). I feel pretty confident that this is the case. Certainly<br>
> more confident than I am in there<br>
> being no inconsistency bugs in the type checker, for instance.<br>
><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' = 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' by<br>
processing lists of macrodigits, add the proofs for the properties (like<br>
say +-comm) for Nat'.<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>