Stream: Coq users

Topic: Comment in ExtrOcamlNatInt

view this post on Zulip Julin Shaji (Oct 28 2023 at 16:41):

In ExtrOcamlNatInt, it is mentioned that:

Disclaimer: trying to obtain efficient certified programs by extracting nat into int is definitively not a good idea:

But upon going to the, the same comment is present.

In ExtrOcamlNatInt, it was also mentioned that:

For serious use of numbers in extracted programs, you are advised to use either coq advanced representations (positive, Z, N, BigN, BigZ) or modular/axiomatic representation.

I suppose int not being infinite is the problem?

What are the other ways to mitigate this? And what does modular/axiomatic representation involve?

view this post on Zulip Julin Shaji (Oct 28 2023 at 18:02):

Could this be related?

But that still seem to be using Z, but with a proof that it is within a bound.

view this post on Zulip Li-yao (Oct 28 2023 at 21:25):

modular means to use one of the cyclic groups, like Z/(2^63)Z. There are many ways to do this. Using a bounded subset of Z is one. Another is to just declare axioms, although they wouldn't compute. Now there is a native axiomatization which does compute.

Last updated: Jun 23 2024 at 05:02 UTC