Roughly speaking, with a deep embedding of a logic, you (1) define a datatype representing the syntax for your logic, and (2) give a model of the syntax, and (3) prove that axioms about your syntax are sound with respect to the model. With a shallow embedding, you skip steps (1) and (2), and just start with a model, and prove entailments between formulas. This means shallow embeddings are usually less work to get off the ground, since they represent work you'd typically end up doing anyway with a deep embedding.
However, if have a deep embedding, it is usually easier to write reflective decision procedures, since you are working with formulas which actually have syntax you can recurse over. Also, if your model is strange or complicated, then you usually don't want to work directly with the semantics. (For example, if you use biorthogonality to force admissible closure, or use Kripke-style models to force frame properties in separation logics, or similar games.) However, deep embeddings will almost certainly force you to think a lot about variable binding and substitutions, which will fill your heart with rage, since this is (a) trivial, and (b) a never-ending source of annoyance.
The correct sequence you should take is: (1) try to get by with a shallow embedding. (2) When that runs out of steam, try using tactics and quotation to run the decision procedures you want to run. (3) If that also runs out of steam, give up and use a dependently-typed syntax for your deep embedding.
- Plan to take a couple of months on (3) if this is your first time out. You will need to get familiar with the fancy features of your proof assistant to stay sane. (But this is an investment which will pay off in general.)
- If your proof assistant doesn't have dependent types, stay at level 2.
- If your object language is itself dependently typed, stay at level 2.
Also, do not try to go gradually up the ladder. When you decide to go up the complexity ladder, take a full step at a time. If you do things bit-by-bit, then you will get lots of theorems which are weird and unusable (eg, you'll get multiple half-assed syntaxes, and theorems which mix syntax and semantics in strange ways), which you will eventually have to throw out.
EDIT: Here's a comment explaining why going up the ladder gradually is so tempting, and why it leads (in general) to suffering.
Concretely, suppose you have a shallow embedding of separation logic, with the connectives $A \star B$ and unit $I$. Then, you'll prove theorems like $A \star B \iff B \star A$ and $(A \star B) \star C \iff A \star (B \star C)$ and so on. Now, when you try to actually use the logic to prove a program correct, you'll end up having something like $(I \star A) \star (B \star C)$ and you'll actually want something like $A \star (B \star (C \star I))$.
At this point, you'll get annoyed with having to manually reassociate formulas, and you'll think, "I know! I'll interpret a datatype of lists as a list of separated formulas. That way, I can interpret $\star$ as concatenation of these lists, and then those formulas above will be definitionally equal!"
This is true, and works! However, note that conjunction is also ACUI, and so is disjunction. So you'll go through the same process in other proofs, with different list datatypes, and then you'll have three syntaxes for different fragments of separation logic, and you'll have metatheorems for each of them, which will inevitably be different, and you'll find yourself wanting a metatheorem you proved for separating conjunction for disjunction, and then you'll want to mix syntaxes, and then you'll go insane.
It's better to target the biggest fragment you can handle with a reasonable effort, and just do it.