I'd recommend people interested in learning formal methods do not start with things such as Coq or Isabelle/HOL. Most people find the process of learning or using those so difficult that they quit with a potentially-permanent aversion to the term formal verification. In engineering, it's often advised to use best tool for the job esp with highest ROI. So, if you're interested in formal methods, I strongly encourage you to start with so-called, lightweight methods that give a lot of return for little investment. They teach you how abstract specifications with tool-assisted reasoning can quickly catch deep errors tests often won't.
Two of those with lots of benefit in realistic projects are Alloy Analyzer (esp for structure) and TLA+/PlusCal (esp for order):
These are immediately useful. Especially in distributed systems for TLA+. Then, you get a book such as Chlipala's Certified Programming with Dependent Types or Pierce et al's Software Foundations. Chlipala is also doing a new one called "Formal Reasoning About Programs." You can try to use those to get some elementary stuff done with the heavyweight methods. It will probably take you 1-2 years to get proficient enough for real stuff. Two outcomes are common:
1. You don't make it. Don't get mad: most don't even when they're smart. Good news is you enjoyed lighter stuff that you'll probably continue to apply and expand on for rest of your career. If other users are lucky, you might have run into their limitations enough to start improving the tooling, documentation, or something else. Those will get better since you learned them but avoided heavyweight stuff.
2. You made it! Now, best result for us IT folks is you apply your skills to real-world software formally-verifying useful algorithms, protocols, compilers, OS's, and so on. For inspiration, be sure to look at CRYPTOL, miTLS, CompCert, CakeML, RockSalt, seL4 or VAMOS, Verdi, verified garbage collectors, foundational backing of static analyzers like Verasco, tools with automation such as SPARK Ada, ACL2 for hardware, and maybe rewriting-based stuff like C semantics in K Framework.
If you can understand heavyweight verification, then apply your knowledge to more stuff like that since you'll (a) possibly be having real-world impact and (b) be doing work challenging enough that you can be very proud of your successes.
I felt obliged to comment because I feel I know what you are talking about and I also worry that much of the advice posted so far is wrong at best, dangerous at worst.
I am 42-year-old very successful programmer who has been through a lot of situations in my career so far, many of them highly demotivating. And the best advice I have for you is to get out of what you are doing. Really. Even though you state that you are not in a position to do that, you really are. It is okay. You are free. Okay, you are helping your boyfriend's startup but what is the appropriate cost for this? Would he have you do it if he knew it was crushing your soul?
I don't use the phrase "crushing your soul" lightly. When it happens slowly, as it does in these cases, it is hard to see the scale of what is happening. But this is a very serious situation and if left unchecked it may damage the potential for you to do good work for the rest of your life. Reasons:
* The commenters who are warning about burnout are right. Burnout is a very serious situation. If you burn yourself out hard, it will be difficult to be effective at any future job you go to, even if it is ostensibly a wonderful job. Treat burnout like a physical injury. I burned myself out once and it took at least 12 years to regain full productivity. Don't do it.
* More broadly, the best and most creative work comes from a root of joy and excitement. If you lose your ability to feel joy and excitement about programming-related things, you'll be unable to do the best work. That this issue is separate from and parallel to burnout! If you are burned out, you might still be able to feel the joy and excitement briefly at the start of a project/idea, but they will fade quickly as the reality of day-to-day work sets in. Alternatively, if you are not burned out but also do not have a sense of wonder, it is likely you will never get yourself started on the good work.
* The earlier in your career it is now, the more important this time is for your development. Programmers learn by doing. If you put yourself into an environment where you are constantly challenged and are working at the top threshold of your ability, then after a few years have gone by, your skills will have increased tremendously. It is like going to intensively learn kung fu for a few years, or going into Navy SEAL training or something. But this isn't just a one-time constant increase. The faster you get things done, and the more thorough and error-free they are, the more ideas you can execute on, which means you will learn faster in the future too. Over the long term, programming skill is like compound interest. More now means a LOT more later. Less now means a LOT less later.
So if you are putting yourself into a position that is not really challenging, that is a bummer day in and day out, and you get things done slowly, you aren't just having a slow time now. You are bringing down that compound interest curve for the rest of your career. It is a serious problem.
If I could go back to my early career I would mercilessly cut out all the shitty jobs I did (and there were many of them).
One more thing, about personal identity. Early on as a programmer, I was often in situations like you describe. I didn't like what I was doing, I thought the management was dumb, I just didn't think my work was very important. I would be very depressed on projects, make slow progress, at times get into a mode where I was much of the time pretending progress simply because I could not bring myself to do the work. I just didn't have the spirit to do it. (I know many people here know what I am talking about.) Over time I got depressed about this: Do I have a terrible work ethic? Am I really just a bad programmer? A bad person? But these questions were not so verbalized or intellectualized, they were just more like an ambient malaise and a disappointment in where life was going.
What I learned, later on, is that I do not at all have a bad work ethic and I am not a bad person. In fact I am quite fierce and get huge amounts of good work done, when I believe that what I am doing is important. It turns out that, for me, to capture this feeling of importance, I had to work on my own projects (and even then it took a long time to find the ideas that really moved me). But once I found this, it basically turned me into a different person. If this is how it works for you, the difference between these two modes of life is HUGE.
Okay, this has been long and rambling. I'll cut it off here. Good luck.
Two of those with lots of benefit in realistic projects are Alloy Analyzer (esp for structure) and TLA+/PlusCal (esp for order):
http://alloy.mit.edu/
https://learntla.com/introduction/
These are immediately useful. Especially in distributed systems for TLA+. Then, you get a book such as Chlipala's Certified Programming with Dependent Types or Pierce et al's Software Foundations. Chlipala is also doing a new one called "Formal Reasoning About Programs." You can try to use those to get some elementary stuff done with the heavyweight methods. It will probably take you 1-2 years to get proficient enough for real stuff. Two outcomes are common:
1. You don't make it. Don't get mad: most don't even when they're smart. Good news is you enjoyed lighter stuff that you'll probably continue to apply and expand on for rest of your career. If other users are lucky, you might have run into their limitations enough to start improving the tooling, documentation, or something else. Those will get better since you learned them but avoided heavyweight stuff.
2. You made it! Now, best result for us IT folks is you apply your skills to real-world software formally-verifying useful algorithms, protocols, compilers, OS's, and so on. For inspiration, be sure to look at CRYPTOL, miTLS, CompCert, CakeML, RockSalt, seL4 or VAMOS, Verdi, verified garbage collectors, foundational backing of static analyzers like Verasco, tools with automation such as SPARK Ada, ACL2 for hardware, and maybe rewriting-based stuff like C semantics in K Framework.
If you can understand heavyweight verification, then apply your knowledge to more stuff like that since you'll (a) possibly be having real-world impact and (b) be doing work challenging enough that you can be very proud of your successes.