<div dir="ltr"><div>I was trying to support floats in agda-ocaml when I realized that this is a lost cause and a very dangerous one.</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>Is it the job of agda to check whether two hardware or software versions have the same computational results? Of course not.</div><div><br></div><div>In my opinion, all platform dependent computations should be inserted as postulates. This way, agda will do exactly what it was programmed to do.</div><div><br></div><div>And we can still prove things for postulates.</div><div><br></div><div>```</div><div>open import Common.Integer<br>open import Agda.Builtin.Equality<br><br>postulate<br>  Float : Set<br>  d : Float<br>  round : Float → Integer<br><br>f : round d ≡ round d<br>f = refl<br></div><div>```<br></div></div>