Platform exploitation is hard to prevent/detect (soundness issue)

[xrchz]

Consider running the following code having built HOL atop Poly/ML v5.9.2:

> val false_thm = RunCall.unsafeCast (Thm.tag $ REFL F_tm, HOLset.empty Term.compare, F_tm) : thm;
val false_thm = ⊢ F: thm
> (Tag.dest_tag $ Thm.tag false_thm, hyp false_thm, concl false_thm ~~ F_tm);
val it = (([], []), [], true): (string list * string list) * term list * bool

If this approach is used somewhere in one's development, it can be hard to tell that the theorem isn't trustworthy.

[xrchz]

A simple mitigation might be to shadow RunCall and Foreign in Overlay.sml:

  structure RunCall = struct end
  structure Foreign = struct end

[konrad-slind]

Nice observation. Brings home that proof validation/verification is a combination of an inference system and a platform it runs on. Both have to bring "good properties" to the table in order for the combination to be trusted.

[xrchz]

For me this is extra motivation for #1825 in the short term at least. (And also for switching to a verified compiler in general (although this particular issue isn't a compiler bug).)

[ordinarymath]

Please allow a way to opt in to use RunCall it's very useful in practice.