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
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