I just came in the comments to recommend that book myself! It has been awhile since I had really took a deep dive into the lambda calculus and I was pleasantly surprised with both how readable this book has been so far (still working through it) and just how much I still had to learn about type systems.

I also had previously thought I wasn't that interest in formal proofs because I was never super interested in traditional mathematical proofs, but once I realize formal proofs can be viewed as an extension of type checking it got me a lot more interested!

Cool! Until recently I also wouldn't have been that attracted by this title, but since learning more about proof theory and logic on one hand, and computation on the other, and beginning to grasp more the depth of the connection/isomorphism between them via the Curry-Howard correspondence, it turns out this book is pretty much exactly along the right path for me now. Next up will be getting a better grasp of how it all relates to category theory via the so-called Curry-Howard-Lambek correspondence...