[tel]

> "Easily debug"

One of the major driving forces in the design of computer proof systems is that they (a) output proofs along with assertions that are (b) trivially verifiable. Indeed, verification is a major philosophical and practical force behind the theory of any type theory.

Ultimately, this is a major component of the design of a proof checker because while lots of its pieces can be complex and scary and potentially buggy, the proof verifier must always be tiny and easy and impeccable because it bears the entire burden of safety.

A similar argument cannot really be made for CAS, I think. Even open source ones.

(There's a catchy name for this principle, but I forget it. "Somebody's Something")