Re: [isabelle] Isabelle Foundation & Certification

On Sun, 20 Sep 2015, Freek Wiedijk wrote:

OCaml is much less safe than SML, e.g. strings are mutable, ints overflow at unspecified word size without any exception,

I think the newest OCaml support immutable strings?

This would be very good news indeed.

And if in the kernel you would use nums instead of ints, then the second problems would be gone too?

The Coq guys are doing that.

In Poly/ML we have int = num by default -- at the bottom there is either the GMP library or an old custom-made implementation. Both can fail in their own right, but it is better to have the idea of proper integers somehow implemented than unspecified machine word arithmetic.

In a discussion with J. Harrison on the HOL mailing list some years ago about proper integers in LCF-style kernels, we eventually agreed that the most robust approach would be to have just 64bit integers with explicit checking (overflow exception), and not bignums.

Note that ML code using infamous catch-all patterns "e1 handle _ => e2" would become erratic in situations of spurious overflow! The Isabelle code base is clear of that (thanks to static checking and warnings in Poly/ML), but I still see it routinely in other provers.

And maybe you only would need to go through nums when you actually calculate with ints in the kernel? Does this even happen, and if so, in which functions?

SML allows in principle to work with fixed-size integers (with overflow exception) or unbounded integers side-by-side. An ultra-safe kernel would use the former, and applications the latter.

We actually used to have such a situation in the past, not on our own choice, but due to SML/NJ imposing it on us. It was very annoying to have limited int here, and bigint there (e.g. for computer-algebra applications). Eventually, I made some efforts to collapse the zoo of int types just to one big int, and we have lived happily ever after.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.