If you are interested in recent developments in verified programming, you might be interested in looking at Adam Chlipala's work (in particular, Bedrock [1]).

If you are interested in recent developments in verified programming, you might be interested in looking at Adam Chlipala's work (in particular, Bedrock [1]). His book "Certified Programming with Dependent Types" is a fantastic resource. Coq can be daunting to start with because it is three different programming languages in one: Gallina is the main pure functional programming language, Vernacular is a language of commands for controlling/guiding the proof assistant, and LTAC is the "type-level programming language on steroids" for writing type-level proofs. ("Type-level" is the important word here - the Curry-Howard correspondence allows us to encode propositions as types, and proofs are inhabitants of those types). When I was getting into certified programming, I found it helpful to try different proof systems until I could understand the common features. I found Microsoft's Lean Theorem Prover [2] to be quite user friendly and well documented, and I liked the syntax and feel. Also, trying out something bare-bones like Twelf [3] can help too, because there is not a lot of extra stuff tacked on and it is closer to an assembly language for machine-assisted proofs. For doing real-world things with Coq such as writing a simple web server, check out Guillaume Claret's blog [4]. Agda is comparable to Coq in terms of what they can do (I have heard). Idris is a "PacMan-complete" language that you might find useful for writing real-world programs, but I am not familiar with its suitability for programs relying on really complex proofs. Edwin Brady is writing a book on Idris [5], and you can get pre-release drafts through the Manning Early Access Program. [1] http://plv.csail.mit.edu/bedrock/ http://plv.csail.mit.edu/bedrock/ [2] https://leanprover.github.io/ https://leanprover.github.io/ [3] http://twelf.org/wiki/Main_Page http://twelf.org/wiki/Main_Page [4] http://coq-blog.clarus.me/ http://coq-blog.clarus.me/ [5] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...