The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I think it is fair to say that having machine-independent integers is a design choice, more than a constraint. We could have written a Coq library where the size of integers is instantiated once and for all according to the architecture. Only proofs relying specifically on the value of this size, and the .vo files, would no longer be portable across architectures.

Well, it is possible but not really reasonable (unless a very very compelling use case, I really don't think it's worth the trouble). Pretty much every proof on machine integers rely on the size of the integers anyway. You may argue that as long as you don't mention it explicitly the v file is still portable as the automated scripts should infer the size. But it would probably need more care than it sounds, some call to auto that terminates instantly for P 31 may very well take ages to succeed on P 63, and things like that.
 

Indeed, and we can do something similar to OCaml's Int64 values, which are blocks with specific ("custom") tags.

Indeed. Ocaml custom tags strike as the right decision, as they cannot be used by constructors anyway. It's robust enough, and following an indirection prior to testing is pretty much free because the cache should work well.
 

I have a very experimental prototype with 63-bits integers (for the regular evaluation machine of the kernel, as well as the VM and the native compiler), but with no emulation support for the VM on 32-bits architectures yet. I gave a talk on this work at the last Coq Workshop: http://www.maximedenes.fr/download/coq_primitives.pdf

The reason why this prototype has not been integrated in Coq's trunk yet is not so much an additional complexity, but rather the desire to take the opportunity to polish the associated libraries. Which is a time consuming task, but seems necessary given their current shape :)

I look forward to it. But you can't deny that it has been more difficult to bring to fruition than the very simple implementation which we currently have.