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 of words.)

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