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

Hi Christoph,

> (BTW, is the Scala code generator actively maintained?  That would be
> great, because our main selling point in using Scala as an output target
> is to demonstrate that such code can easily be integrated with
> business-ready software.  This is work in the context of formalising
> auctions, see
> so we need to convince people who may never heard of SML, OCaml and
> Haskell, but have heard of Java.)

Concerning »actively maintained«, there is somebody (namely me) who will
look after your issue.  I welcome your effort to carry Isabelle out of
the ML/Haskell subculture, but there is one caveat: the code generator
for Scala translates HOL's calculus into a functional Scala program
without attempting any transformation to idiomize it towards Scala as
written by experienced Scala programmes.  For illustration, have a look
at the generated code.  I never heard of any reports how feasible the
code is to incorporate in bigger Scala applications.

Stay tuned,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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