Re: [isabelle] “Programming in Isabelle/HOL”

On Wed, 19 Feb 2014, Yannick Duchêne (Hibou57) wrote:

I will avoid posting it in other places (unfortunately, I already posted it on StackOverflow yesterday, in a comment).

In the worst case you can delete notes on StackOverflow.

For the next group of students this page will undergo essential updates --- for compelling reasons!

I've looked through the notes for 5min. Something in education must have gone utterly wrong if people are more familiar with WHILE, GOTO, poking around in memory than just plain and basic functional recursion.

Just one technical note: the ancient PolyML.makestring is used, but that is long obsolete. It has probably been passed around as a special secret from Isabelle/ML users in ancient times, but the documented way is the @{make_string} antiquotation (see implementation manual):

  The ML compiler knows about the structure of values according
  to their static type, and can print them in the manner of the
  toplevel loop, although the details are non-portable.  The
  antiquotation @{ML_antiquotation_def "make_string"} provides a
  quasi-portable way to refer to this potential capability of the
  underlying ML system in generic Isabelle/ML sources.

As usual for all newer Isabelle output facilities, proper pretty and markup information is used, as far as available from ML toplevel pretty printers. I.e. you get decent output in the Prover IDE, unlike the bare-bones black-and-white PolyML.makestring, so please forget the latter.

Of course, printing ML values in the notation of the compiler is mostly for experimental and informative purposes. Giving such raw output to the end-user would be unpolite. (Java and Python programmers do this routinely, but not the ML elite.)


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