Consider a reasonable type theory $T$ with decidable checking. Think of it as the core type theory implemented in the kernel of a proof assistant, i.e., with fully elaborated and annotated judgements that nobody wants to write with bare hands.
A central task of formalization is inhabitation of a type: given a derivable judgement $\Gamma \vdash A \; \mathsf{type}$ (the goal), the user provides an expression $e$ (the solution), and the kernel checks whether $\Gamma \vdash e : A$ is derivable. How can we do this in a practical way?
It is not practical for the user to write down a fully annotated term $e$. Instead, they write down an expression $c$ in a surface language $V$ (the vernacular) which is elaborated or evaluated by the proof assistant to give a fully annotated expression $e$. In order to account for the possibility of a user error, the proof assistant can be seen as a map
$$\textstyle
P : \prod_{\Gamma, A} \, (\Gamma \vdash A \; \mathsf{type}) \to V \to \{\mathsf{error}\} + \sum_{e} \, (\Gamma \vdash e : A).$$
We read the above as: given a derivable type $A$ in context $\Gamma$ (the goal) and an expression $c$ of type $V$ (the suggested solution), the proof assistant either recognizes that $c$ evaluates to an expression $e$ such that $\Gamma \vdash e : A$, or it reports an error.
Actually, apart from errors, there could also be other computational effects, such as non-termination, state, user interaction, etc. We thus generalize the above to a suitable computational monad $M$:
$$\textstyle
P : \prod_{\Gamma, A} \, (\Gamma \vdash A \; \mathsf{type}) \to V \to M(\sum_{e} \, (\Gamma \vdash e : A)).$$
With the general setup explained, we can address the question. What kind of proof assistant one gets depends on the design of the vernacular $V$ and the computational monad $M$. Some possibilities are:
Agda: to give the user the impression that they are working with $T$ directly, we design the vernacular $V$ to look like an abridged version of $T$ and call the expressions of $V$ (proof) terms. The computational monad $M$ supports interactive construction of terms through ”holes“ that represent subgoals. (Agda also support meta-programming through which the user can implement proof search and other techniques that people call “tactics”.)
Coq and Lean: make the vernacular $V$ look like a command-based programming language. The commands are called tactics. The monad $M$ incorporates the current goal as state that is manipulated by the user through tactics. The command-based language allows general recursion and construction of non-terminating programs.
Isabelle/HOL: make the vernacular $V$ look like a meta-level programming language. There is a built-in abstract data type of judgements, which is controlled by a trusted kernel. The user writes programs that evaluate to judgements. There is a library of useful functions for constructing judgements, called tactics. The user is free to implement their own functions, as well as Tetris.
Reflection is the ability for the vernacular $V$ to access the abstract syntax trees of computed judgements. Again, there is more than one way of doing this:
(If someone can provide better descriptions and links to reflection for Lean and Isabelle, that would be grand.)
Reflection is not to be confused with Boolean reflection, which is a proof technique for (ab)using the equality checker as a decision procedure. Please ask a separate question if you'd like to know more.