Nowadays one can hope to write real programs, prove them correct with mechanical checking, compile them with a proved (and mechanically checked) compiler, and therefore get strong guarantees about what actually runs on the hardware. If one chooses to use an imperative language such as C (which is certainly not the only obvious choice), a shallow embedding of Separation Logic in Coq seems a reasonable approach. I will discuss engineering solutions to the problems that must be solved when Separation Logic is used in a tactical higher-order logic theorem prover, to prove correctness and not just safety, on a full-scale programming language in which expressions have (read) side effects.