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.

Cheers,

Christoph

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
  http://cicm-conference.org/2013/
→ Modular Ontologies (WoMO), 15 September, Corunna, Spain.
  Submission until 12 July; http://www.iaoa.org/womo/2013.html
→ Knowledge and Experience Management, 7-9 October, Bamberg, Germany.
  Submission until 15 July; http://minf.uni-bamberg.de/lwa2013/cfp/fgwm/
→ Mathematics in Computer Science Special Issue on “Enabling Domain
  Experts to use Formalised Reasoning”; submission until 31 October.
  http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/




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