Programming in the 1990s by Edward Cohen is an interesting book for introducing software developers to a method of proof writing by way of predicate calculus. I

Programming in the 1990s by Edward Cohen is an interesting book for introducing software developers to a method of proof writing by way of predicate calculus. It's a book one can read from cover to cover. The TLA+ book by Leslie Lamport is also an interesting read even if it is specific to a particular logic for creating specifications. Any of his talks on TLA+ are also good for a high-level overview of the why and a bit of the how as well.