Re: [isabelle] Rational numbers in Isabelle/ML

I would say bad, and we should try to limit our deviations from Standard ML to what is essential. If there ever is further evolution of Standard ML, we should try to bring our own ideas into it.

CakeML illustrates the advantages of a formal definition. It is a subset of standard ML with substantially the same semantics. Without a formal semantics, the very idea of a verified compiler is meaningless. Others have also noticed the benefits of using a formally defined language for coding a theorem prover. We have been forced to stretch things a bit, due to the lack of other competitive implementations, but we must hope that this situation doesn't last forever.

Larry Paulson

> On 1 Apr 2016, at 23:10, Makarius <makarius at> wrote:
> This means that standard-ness is given up, and the game becomes more like that of OCaml (or Scala, even Haskell/GHC). I am myself still unsure if this is good or bad.

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