Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
On Thu, 4 Jul 2013, Manuel Eberl wrote:
On 07/03/2013 11:46 PM, Christoph LANGE wrote:
I am nowhere near an _experienced_ Scala programmer yet, but
sufficiently capable of writing wrapper functions that, e.g., convert
set[Nat] to List[Int] […]
At the danger of being called a nitpicker: this sort of thing can cost
you the programme correctness that you have so painstakingly ensured
with Isabelle, since Int in Scala is subject to integer overflow. I have
heard stories of "verified" code producing horribly wrong results
because people did not take integer overflow into account.
The funny thing is that the type called "Int" or "int" in most real-world
programming languages is not for integers at all, but for machine words.
The JVM platform is in a relatively good situation here, because that is
precisely specified as 32bit signed word-arithmentic. So overflow is not
an accident, but part of the algebra on that particular type. (There are
also celebrated books about making really smart things with that algebra
Surprise only starts, when people use that word type as approximation for
proper ints. There are historical and technical reasons for doing that by
default on the JVM: BigInt is much less efficient on that platform, due to
the physical distinction of base types vs. object types at runtime.
In SML the situation is much better: type "int" means mathematical
integers, without implicit overflow, and the implementation is quite fast:
for small values it uses fast machine arithmentic, for big values it
silently upgrades to a library (here GNU MP, which is also quite fast).
This archive was generated by a fusion of
Pipermail (Mailman edition) and