The book assumes a bit of familiarity with the subject and isn't bureaucratic in formality. Many ideas are hard to present formally or aren't even understood formally yet. I find the informal discussion in this book very valuable. It allows to see the motivation behind logic beyond text-crunching right from the beginning.

A closed term is one where all variables are bound (no free variables). Abstraction is a lambda-expression.