Introduction to Theoretical Computer Science (introtcs.org)

I love the approach of using a programming language as the model of computation, instead of Turing machines or RAM models. The credit for this idea belongs to Neil D. Jones and to Amir Ben Amram, for whom Boaz Barak was a TA back when Boaz was a grad student.

This is a very nice introduction, but it could definitely benefit from some perspective from the other side of computer science (PLs/types-land). E.g., the section on "beyond computing functions" could also discuss how such things can be nicely modeled using monads.