The goal of the Automath system (developed at Eindhoven from 1967 onwards) was to develop a framework for expressing mathematical theories in a form that enables a computer to verify the correctness. The fundamental idea is that whatever is said correctly, is correct. There is no other norm for correctness.
Unless the language structure is called the logic, the Automath system itself contains no logic and no mathematical foundations. All material necessary for mathematics are to be explained in the books to be written in the language. The rules of the language do not go beyond the ideas of a typed lambda calculus, and it is in terms of such typing that the meaning of notions like "definition", "theorem", "proof", "axiom" have to be understood. A complete book is structured as a collection of nested blocks, where opening a block can be seen as the introduction of a typed variable. Such variables can represent mathematical objects or mathematical proofs, and the reference systems for those emotionally very different entities turn out to be completely similar. That was how the idea of "proofs as objects" got into the system from the start.
Having and interpreting this block structure is the only thing that could be called prerequisite logic. All the rest of logic, and the foundation of mathematics, is book material. Automath presents a novel way of treating logic and its relation to mathematics. The system can be handled in a very natural way, directly derived from our mathematical habits. It can therefore have an educational spin-off. The art of teaching mathematics to students can learn from the precise way in which we have to talk to a machine in this system without logical or mathematical prerequisites.
The Automath system never claimed to automate the invention of mathematics, not even to automate the construction of proofs of given theorems. The Automath correctness checker is just a careful reader of well-presented finished material.