This looks like it's (going to be) about a theory of programming languages as based on some form of the lambda calculus. I think it doesn't get pointed out enough that this is not a descriptive science but more of a normative theory with mathematical elements. It doesn't try to analyze and compare existing programming languages. It asserts how they ought to be and derives consequences from this. In this sense, it's less like the theory of evolution and more like a political or aesthetical movement.
Wadler himself seems to dislike calling this "computer science": "You don't put science in your name if you're a real science." I'm quite sure he meant it differently, but it fits my argument to quote him out of context :)
The book itself is still unfinished obviously. Most of it seems to be a formalization of the absolute basics of constructive logic currently. I'm also not sure how far they are really going to go here; feasibly formalizing the meta theory of agda (Martin-Löf type theory) in agda itself seems to be an open problem. Yes, seriously.
I found agda much less opaque than coq and especially isabel. It seems much more cumbersome to work with in practice though. I doubt agda will ever be used for serious proofs beyond hello world or very specialized areas as long as there is not more automation... at which point you're back at a variant of coq.
Wadler himself seems to dislike calling this "computer science": "You don't put science in your name if you're a real science." I'm quite sure he meant it differently, but it fits my argument to quote him out of context :)
The book itself is still unfinished obviously. Most of it seems to be a formalization of the absolute basics of constructive logic currently. I'm also not sure how far they are really going to go here; feasibly formalizing the meta theory of agda (Martin-Löf type theory) in agda itself seems to be an open problem. Yes, seriously.
I found agda much less opaque than coq and especially isabel. It seems much more cumbersome to work with in practice though. I doubt agda will ever be used for serious proofs beyond hello world or very specialized areas as long as there is not more automation... at which point you're back at a variant of coq.