Re: [isabelle] Some Remarks to Code Generation
Le Tue, 31 Jul 2012 18:13:12 +0200, Patrick Michel
<uni at pbmichel.de> 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
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and