Why do we need tactics, reflection and other techniques when we have Curry-Howard for theorem proving?

Question

First of all, I apologize if this question is slightly misplaced, but this seemed the best place to ask it given the mathematical/theoretical nature of the discussion. Given that the Curry-Howard correspondence tells us that terms of certain typed lambda calculi serve as proofs of the logical statements that their types embody, it seems that hypothetically such a programming language should itself be a fully functional theorem prover. What I have been able to find seems to indicate this is the case and the addition of other technologies like tactics languages or reflection are matters of pragmatic rather than tehoretical necessity. In other words, they make writing certain proofs much faster, though it is possible to write the same proofs in the raw language itself and the proofs are often represented internally this way. So my question roughly is whether or not I am correct in my conjecture about dedicated proof languages/techniques being theoretically unnecessary, and if so, what are some examples of practical mathematical/logical problems that make the auxiliary facilities desirable? Along with this, how do these added technologies relate to the base language? I understand Ltac is an untyped imperative language that allows a sort of meta-programming by interactively manipulating terms of Coq's base language in logically sound ways, but I am not certain how the tactics themselves are known to be sound since they are part of a separate untyped language and I am even less clear on how reflection in languages like Agda relates to the "non-proof" parts of the language. Thank you for any insight you could provide on any of these points.

Answer 1

Tactics are important for the pragmatics of flexibility and maintainability of larger scale projects, you can learn about it in CPDT. There are no soundness criteria needed for tactics as they just build up constructions which the type theory then checks and will reject if they are invalid.

Reflection is separate from tactics - it is a consequence of the language having functions of dependent type. If you define an interpretation function that reflects some syntax into meaningful statements (types) you may also be able to write a function that takes some syntax and maybe produces a proof (inhabitant) of its interpretation. You may see an example of this in Proofs of correctness in Mathematics and Industry - Henk Barendregt. Reflection may be used in the same way as a tactic but it much more formal and in accordance with Godel expressing more of the full type theory in terms of itself becomes increasingly difficult.