FStarLang
Floating point literals are badly handled by the F# extraction mechanism
Using literal floating point in some meant-to-be-extracted file like the F* compiler can produce bad results when extracting with the F# version of the F* compiler (seems to be fine with the ocaml version). For example 1.0 is extracted to 1 and 0.99 to 0,99 which are no longer of the same type. A temporary solution is to use float_of_string "1.0" but I would be rather surprised if there is no better way to do that in F#.
Why are we parsing floats as floats? We should preserve them as strings, just like we do for machine integer literals, otherwise we're going to go through IEEE-754 rounding, possibly depending on the rounding mode of the compiler, not the runtime rounding mode of the program...?
Indeed integers are kept as strings but floating point numbers are interpreted directly. We might want to change that.
Yes. Also, it may be the case the in .NET lingo float means IEEE-754 simple precision. (That would explain your behavior.)
hi @ShalokShalom , I think @mtzguido is also commenting about this on other issues.
You may have misunderstood the situation: We support extraction for F* code to F# and plan to continue doing that, although we could use help in improving & maintaining it.
And what is not supported than anymore?
You should really document that somewhere properly.