This is a collection of links and notes on programming and formal verification with dependent types. Both those activities are an interesting hobby, and potentially useful in professional programming (though as of 2019, perhaps the tools are still not mature enough to use for everyday programming tasks).
Software Foundations by Benjamin C. Pierce and others is a good introduction, using the Coq proof assistant. It contains interactive exercises, is well-written, and does not require prior familiarity with the topic.
Type Theory and Functional Programming by Simon Thompson is an older book (from 1991), which is rather nice and comprehensive, but still begins with the very basics, and also freely available.
Sequent calculus is frequently used in type theory textbooks and papers, and Logitext provides a nice interactive tutorial. Since dependent typing is usually done on top of lambda calculus, familiarity with it is important as well, but I think nowadays it is rather common. Though Structure and Interpretation of Computer Programs by Abelson, Sussman, and Sussman can be mentioned here as a good (functional) programming introduction, and one can just poke functional languages such as Haskell or Scheme for an interactive playground (in which it may be useful to play with Church encoding).
Some languages (such as Coq's Gallina) target primarily proof assistants, and/or rely on less elegant techniques and typing (SMT solvers, types only depending on natural numbers, etc). The modern (actively maintained) ones that are both closer to common programming languages and feel closer to the theory (i.e., don't hide it under "tactics") are Agda and Idris, with the latter explicitly trying to be suitable for practical programming.
Coq, Agda, and Idris have decent Emacs modes, and I hear Idris is often used with vim as well. Their compilers and libraries are not necessarily straightforward to build and setup, but not particularly painful either. All three have IRC channels on Freenode/Libera.chat (#coq, #agda, #idris), with active and helpful communities. The situation with mailing lists and documentation varies.
Back in 2014, I've also composed an Idris overview (in Russian, not assuming familiarity with either type theory or functional programming).
To better connect the basic theory to actual languages, it is useful to learn how they are implemented. Of course there is the code of compilers themselves, but just jumping into it is not a great way to learn. Omitting general programming language theory, I will list the articles and papers I found to be helpful for learning about implementations of dependently typed languages in particular.
"Simpler, easier!" is a good article to begin with, providing and explaining a very basic implementation. One can add data types as axioms, possibly some syntax and function/operator overloading, and get something resembling a language. "Implicit arguments" in the old Coq documentation describe different types of implicit arguments, hinting how they work and can be added as well.
A Tutorial Implementation of a Dependently Typed Lambda Calculus is more comprehensive and detailed, containing many references.
Pi-Forall is a basic educational language with dependent types, implementation documentation (including quite a few useful references), and corresponding lectures. And there are other small dependently typed languages, such as nano-Agda.
Then there are papers, often by authors of those languages: Thierry Coquand (Coq), Ulf Norell (Agda), Edwin Brady (Idris).
Homotopy type theory is a cool new subject, at least for the past few years. The last time I checked, it wasn't quite clear how applicable it is to computations, and I didn't even get far into the HoTT book, getting rather tired and bored after trying to learn algebraic topology basics (on which HoTT is based).
Category theory is often employed in functional programming, and with dependent types algebraic structures can be defined nicely, together with properties of their operations. It is also related via Curry–Howard–Lambek correspondence, which is fun to explore and has some applications, but sometimes its usage in FP reminds me of building factories of factories in OOP.
Z notation and newer TLA+ seem to be more popular (or at least more widely known) for formal specification and verification, yet both seem quite awkward and limited: Java tooling, first-order logic, ZF set theory, not intended for program extraction, generally much less elegant than languages with dependent types.
Metamath is quite simple, generic, and interesting (based on substitution, does not include any axioms in its core), and its proof checker is written in C (fast and easy to build). Metamath Proof Explorer Home Page contains something resembling an introduction, and there is the Metamath book.
SMT solvers and theorem provers based on those (e.g., Z3 Theorem Prover): can be mixed with languages supporting dependent types, but usually the former focus on bruteforcing a solution, while the latter -- on checking it, often leaving solution/proof to a programmer. But they are also be useful (and less of a bruteforce) for tasks where finding a solution is needed, like one to a system of non-linear equations, not proving a theorem.