[Agda] Platform Independent proofs.

[Philipp Hausmann]

Hi

You are right in so far as the floating point primitives implementation 
needs to exactly match the Haskell implementation used by Agda. Do you 
have a concrete example where this poses a problem?

There are people taking advantage of the fact that Floats can be 
reasoned about [1]. I do think that is a valid use case. This would no 
longer work if Floats were postulates. Note that Agda does not stop you 
from defining your own Float type with postulates. You are also not 
required to implement the float primitives if there is no reasonable way 
to support them.

I feel my comment from #3749 also applies here:

> Is this actually an issue Agda itself needs to solve? Maybe this is a 
> problem libraries should solve, as it already today is possible to 
> package the Float implementation in a record and provide different 
> implementations. Maybe Agda should just provide the single-nan 
> primitives /for now/ because they are the most portable ones and let 
> libraries experiment with packaging it up or adding different 
> implementations? [2]


Cheers
Philipp

[1] https://github.com/agda/agda/issues/2194#issuecomment-251525747
[2] https://github.com/agda/agda/issues/3749#issuecomment-489795629


On 5/23/19 1:22 AM, Apostolis Xekoukoulotakis wrote:
> I was trying to support floats in agda-ocaml when I realized that this 
> is a lost cause and a very dangerous one.
>
> If I didn't match the exact computational results of haskell, then I 
> could get proofs that typechecked in agda that were completely wrong 
> in OCaml.
>
> But there is also a theoretical error in all of this. Right now, we do 
> not have universal proofs like in Mathematics. We have platform 
> dependent proofs.
>
> In other words, we should write explicitly that this proof is correct 
> for this specific version of the CPU, this specific version of haskell 
> etc.
>
> Is it the job of agda to check whether two hardware or software 
> versions have the same computational results? Of course not.
>
> In my opinion, all platform dependent computations should be inserted 
> as postulates. This way, agda will do exactly what it was programmed 
> to do.
>
> And we can still prove things for postulates.
>
> ```
> open import Common.Integer
> open import Agda.Builtin.Equality
>
> postulate
>   Float : Set
>   d : Float
>   round : Float → Integer
>
> f : round d ≡ round d
> f = refl
> ```
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190523/d6cbe31d/attachment.html>