Re: [isabelle] Splicing runtime ML values into Isar



> Can a malicious attacker with access to the ML name space Âhijack your
> evaluation machinery, e.g. by defining it own structure
> Typed_Evaluation?  This is something difficult to handle?

Yes. This may also happen to the "tactic" method:

  MLâ
    structure Method = struct
      fun set_tactic _ = I
    end
  â

  lemma True
  apply (tactic âall_tacâ)

  (* exception Fail raised (line 284 of "Isar/method.ML"):
     Undefined ML tactic *)

Hygiene is often a problem in languages which support nesting and
(anti)quotation of language elements.

Cheers
Lars




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