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

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.

-
Probably the same reason that one needs to do something other than brute force search through all possible moves to depth $n$ to build an effective chess-playing program. –  André Nicolas Dec 3 '12 at 2:52