Arc Forumnew | comments | leaders | submitlogin
2 points by almkglor 6182 days ago | link | parent

Okay, here's a better way of presenting it:

  (def-B&D-type theorem create-theorem (f)
    (if (check-f-is-valid-theorem f)
        (annotate 'theorem f)
        (err "Not a valid theorem")))
Where def-B&D-type is:

  (mac def-B&D-type (type constructor . body)
    (w/uniq real-annotate
      `(let ,real-annotate annotate
         (let annotate ,real-annotate
           (def ,constructor ,@body))
         (= annotate
            (fn (type obj)
              (if (is type ',type)
                  (err "Spank!  Spank!  Under the boots of your master!!")
                  (,real-annotate type obj)))))))
Note however that even under this, it's still possible to redefine 'check-f-is-valid-theorem.

For that matter, it's still possible to defeat "safety" in language X: just implement a version of language X which doesn't have that safety.

In practice, nobody will bother to do (annotate 'foo something-which-is-not-a-foo) anyway.