Re: [isabelle] Clone detection for Isabelle theories



Hi.

Quoting out of context, on purpose:

> ... Isar is very much like Perl.

Great! Use this for advertising.
Should open up a whole new population of users ...

User-defined syntax is perhaps
more a matter of readability
(I guess it's mostly about operator precedences,
and a few special forms - unless you actively abuse it).
But code injection really scares me.

Mind you, Haskell is scary too, because I can do

{-# language TemplateHaskell #-}
import Language.Haskell.TH
$(runIO (print 42) >> return [])
main = return ()

which will do IO during compilation.

But that needs the language pragma to be present
(at the start of the file)
and I can call ghc (the compiler) with "-XSafe"
and it will reject such code outright.

This "safe Haskell" is a recent addition
to the language (well, to GHC actually).
https://ghc.haskell.org/trac/ghc/wiki/SafeHaskell

I wonder why Isabelle plans to abandon
its "safe" flag (as Lars mentioned in
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00034.html
)

Best regards, Johannes.





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