Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions

2013-07-03 23:38 Manuel Eberl:
> 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.
> …
> Personally, unless I do some heavy number-crunching, I use the
> arbitrary-precision Integer type (in Haskell) just to be sure –
> especially with Isabelle-generated code.

Thanks for pointing out.  Indeed BigInt would be the right type to use
in Scala.



Christoph Lange, School of Computer Science, University of Birmingham, Skype duke4701

→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
→ Modular Ontologies (WoMO), 15 September, Corunna, Spain.
  Submission until 12 July;
→ Knowledge and Experience Management, 7-9 October, Bamberg, Germany.
  Submission until 15 July;
→ Mathematics in Computer Science Special Issue on “Enabling Domain
  Experts to use Formalised Reasoning”; submission until 31 October.

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