I'm also currently interested in this area, and I would recommend Interactive Theorem Proving and Program Development. At the same time, it is practical and theoretical.
Adam Chlipala's 'Certified Programming With Dependent Types' is a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation:
http://www.labri.fr/perso/casteran/CoqArt/index.html