I have a MSc with a specialization in formal methods from a place with famous faculty in the field, so I might be biased. But I have to disagree with almost anyone here.
Formal methods still lack a bit of maturity and streamlining to get adopted. It's a bit like functional programming in the late 90s and early 2000s. Nothing was terribly different from now, yet it was not widely used. Whereas now, we are starting to see adoption by mainstream players. E.g. lots of features in Swift.
With regards to formal methods, the situation is entirely analogous. The theory is there. Already developed. And it sits at the absolute core of CS. It's all about formally describing semantics. There are several approaches: type systems, model checking, program analysis and abstract interpretation. And these offer a tremendous amount of flexibility. You can go all the way from adding some lightweight formal specifications a posteriori with e.g. a fancy type system, to developing all your code formally by starting with some axioms.
Altering a habit by means of will-force is not easy.
One simple route can be to make checking some sites more difficult, so that you need to make an effort to log into e.g. Facebook.
For example, you can use Temporary Containers [1] so that all cookies are deleted when you close a tab. Hence, every time you open a new tab and go to facebook.com you will need to make the effort to log in. As a side effect, this approach reduces tracking by third parties.
The obvious route for self-study is to go through Halmos or Axler and Rudin, plus all additional materials and study aids such as Gelbaum & Olmsted, emulating the most popular Harvard Math 55 incarnation. Another nice Math 55 incarnation covered Hubbard & Hubbard, which is a wonderful book.
Although Math 55 is tough, if you are self-paced and have a bit of mathematical maturity I think it is doable. It's also an excellent pure math bootcamp that gives you a solid foundation to branch into any other pure or advanced math topic.
I have gone through Halmos & Rudin myself, and it is a great experience. However, if your end goals are more geared towards pure CS, an alternative route might be much more appropriate. Very interesting and promising parts of CS, such as formal methods, and the foundations of mathematics themselves depend on abstract algebra and logic: https://ncatlab.org/nlab/show/computational+trinitarianism
A minor problem is that beginner literature is not so polished as it is relatively young. But there are some excellent textbooks nonetheless. Some below. Other suggestions welcome:
Formal methods still lack a bit of maturity and streamlining to get adopted. It's a bit like functional programming in the late 90s and early 2000s. Nothing was terribly different from now, yet it was not widely used. Whereas now, we are starting to see adoption by mainstream players. E.g. lots of features in Swift.
With regards to formal methods, the situation is entirely analogous. The theory is there. Already developed. And it sits at the absolute core of CS. It's all about formally describing semantics. There are several approaches: type systems, model checking, program analysis and abstract interpretation. And these offer a tremendous amount of flexibility. You can go all the way from adding some lightweight formal specifications a posteriori with e.g. a fancy type system, to developing all your code formally by starting with some axioms.