World's smallest (Exception-based) proof-checking language (in Python). In what way is Coq, Lean, Isabelle "better"?

Question

As you may already know, the codebases written for Coq, Lean, etc. are humungous. Thus a goal in a new proof assistant might be to simplify things. Suppose we restrict our attention not to general proof theory but to categorical contexts. The closest concept I can think of would be a "CAS for category theory (with proofs)".

C = Cat('C')
X = C.ob('X')
i = Id(X, 'i')
j = Id(X, 'j')

with Proof(goal=Eq(i,j), given=[C, X, i, j]) as p:
    eq1 = p.equals(i, j(i))
    eq2 = p.equals(j(i), j)
    p.QED(p.transitivity(eq1, eq2))
    
print(p.proposition_text())
print(p.proof_text())

The idea is that print will present precisely the following text to the user:

Prop. Let $C$ be a category, $X$ an object in $C$, and $i,j$ identity morphisms on $X$. Then $i = j$.
Proof. $$i = i\circ j \tag{1}$$ $$i\circ j = j \tag{2}$$ Therefore, $i = j$ by transitivity of equality and (1), (2) $\blacksquare$

Thus the most basic proof in Category can be given in English using classes Ob, Cat, Arrow, Id, Proof, and Eq. The methods of the proof instance p encode how to work with and return equalities.

Thus a proof of a statement is valid if and only if we can construct the statement's goal data.

Questions. Would you consider using such a python library as a student of category theory? How would Coq, Lean, or Isabelle be superior on this particular proof? The last question is so that I can make changes to the design, so that it is on par with the other proof assistants.

---

How does proof checking work? Each method call on the p object will perform a run-time assert of the proposed equality against the given equalities. Inclusion of i,j into the givens automatically includes their definitional equalities. Should any assertion fail, the mathematician (or coder / you) will be informed in their IDE of the AssertionFailure. So that is the proof-checking mechanism - it makes use of the exception system within a programming language, which is in this case Python's.

If the with block is exited without a successful call to p.QED then a ProofError will be thrown (another exception). The data of the argument to QED must equal p.goal.

Simply doing p.equals(i,j) from the start will result in a ProofError, since the reference i does not equal the reference j. That is to say, a real proof environment is indeed formed - a.k.a. you can't cheat on a proof.

Answer 1

This thing would be possible. I really struggle to believe it would be remotely as ergonomic as e.g. Lean, though. Phrasing your proofs as types in a strong type system gives the compiler perfect knowledge, and allows it to be extremely helpful (if you haven't experienced Agda or Idris's hole-filling, it is actually miraculous). The extremely dynamic nature of Python means you are crippled from the start. If the user promises they will stick only to using your built-ins, then sure, you could get an experience like Lean's or Coq's where the interactive proof assistant tells you all the information available, but you're embedded in Python where anything goes, so it's quite a bit of trust you're putting on the user.

Additionally, Python is based around mutable state. Your proof terms are inherently dynamic, and the fact that your language is running inside Python means you are inviting the user to knit together proof terms using mutability. I do not believe this will lead to readable or maintainable proofs, and it also makes the job of the kernel a lot harder: if I construct a proof term in function f, then I use it in proof h, then I mutate it in function g, you're going to have to track this somehow so that you can re-evaluate the construction of h. This sounds like a pretty big undertaking to me, not that I'm deeply familiar with Python's reflection APIs. An immutable language rules out this entire can of worms.