Arc Forumnew | comments | leaders | submitlogin
2 points by rocketnia 2961 days ago | link | parent

Well... the axioms of Arc are enumerated in the source code. But that might not be satisfying unless you think Racket is a simple metatheory. :)

Even mathematical axiom systems are always in terms of some metatheory, and the metatheory itself might be in doubt. There's no right answer.

That said, Arc's implementation in terms of Racket is rather large and ad-hoc, and Racket's own implementation is rather large and ad-hoc. There are nicer foundations than these already, like Martin-Löf type theory.