Re: [isabelle] Some Remarks to Code Generation

Le Tue, 31 Jul 2012 18:13:12 +0200, Patrick Michel <uni at> a écrit:
As it turns out it is quite easy to prove a code equation that obviously leads to non-terminating execution.

I've not reached that point (still learning Isabelle and HOL), but I'm already interested in this, as I will generate SML programs from proofs. Can you please, provide a concrete example of an erroneous proof of a non‑terminating function?

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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