What makes a proof assistant a proof assistant?

You open a code editor, define a syntax with lambdas, a few primitives. Then you invent some nice computation rules, some cool typing rules, and write a corresponding interpreter and "type checker". Congratulations! You just built a proof assistant! Now you can formalize all of mathematics on it! Or can you? After all, what makes the thing you built a valid "proof assistant"? What constitutes a "type checker"? As far as I'm concerned, you could have actually implemented Tetris, claimed that blocks are terms, their shapes are types, and the game loop is the computation rule. Who has authority to argue you're wrong?

When it comes to implementing a "programming language", the definition is much more clear. Just invent a syntax, a set of reduction rules and prove your thing Turing-complete. Then it is as good as a programming language is expected to be. When it comes to implementing a proof assistant, I have no idea. Sure, there are common things I see present in proof assistants, so, intuitively, I know what they are. They have lambdas and the corresponding dependent function space, they have inductive datatypes and their introductions and eliminations, and they must be consistent, which mean at least some type is uninhabited. But what if my "proof assistant" has no lambdas nor datatypes? It could have for example just combinators. I don't have a precise definition of what makes a "type theory" a "type theory".

What, formally, makes a program a valid proof assistant, in the same sense that Agda/Coq are? What is a precise and complete definition of a type theory? And what one must do to "justify" his syntax, reduction and typing rules? I'm making this specifically because, while I feel like I can, given enough time, implement something like A Cosmology of Datatypes, I do not feel the freedom to make any change, even minimal, to whatever the author did, because I do not know what justifies those things he did.

I would expect a proof assistant to provide:

• a syntax to express some mathematical statements

• a syntax to express a proof of one of those statements

• a computational process to "check" that a proof of a statement is indeed valid (returns success or failure, or maybe does not return at all)

Finally, for such a proof assistant to be trustworthy, it should come with a justification of the fact that when its checking process says that a proof of a statement is valid, then indeed this statement is valid in the usual mathematical sense -- there exists a mathematical proof that mathematicians will accept.

StackExchange Computer Science Q#97378, answer score: 8