I am also starting to learn, and I don't know if it can be applied to my real problems.
I chose the Lamport learning path. I love that guy and how he thinks and writes. I am reading the book (I bought it in paper, but there is a free version online), watching the video courses, and reading the PlusCal tutorial online.
I enjoy the path and the enlightenment when describing a system with math. Human language has too many ambiguities, very little precision, and is verbose to express some ideas.