As an amateur, I have heard differing opinions on this topic, but I quite enjoyed working through the "Software Foundations" book: https://softwarefoundations.c

As an amateur, I have heard differing opinions on this topic, but I quite enjoyed working through the "Software Foundations" book: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/. This book uses the Coq proof assistant to work through simple example proofs. If you stick with it for a while, the puzzle of finding proofs and getting instantaneous feedback from the assistant becomes quite an enjoyable process.