My TLA+ Saga

This year mark’s my 3rd attempt to learn TLA+.

The first time was likely around the same time Hillel Wayne also discovered it. Although where Hillel (obviously) grokked it the first time, when I discovered that TLA+ is not a tool for auto-generating property based tests, I quit.

The second time, I attended the TLA+ conference in 2019. I was better prepared to understand the purpose of a spec. This is, in part, because I was aware of the “big picture” of the day-job’s work. Where I had work in aviation, and and embedded systems for awhile, I was compartmentalized. Understandably so as I earned more experience, however I was unprepared to understand large scale the purpose of a specification. 2019 I was just starting to see the value. However, I had a second personal hurdle: I was “self taught”.

Being “self-taught” was a point of pride for me. I encapsulated my value to an team by my ability to understand new ideas and be effective reasonably quickly. So much so, that I realized I would hamper myself my not asking for help so I could carry the badge of “I’m self taught”. Guess what, no one cares. If you learn something with a group, from a teacher, or on your own… NO ONE CARES.

Also, it was at least partially a lie. Up to this point, I told myself: “taught myself C++”. Ya, no. I was surrounded by colleagues who knew a plethora of languages: Python, Go, D, C. Yes, I would self-study, but being surrounded by those who can provide a contrast for your own understanding of a material is invaluable!

This third time, I posted to reddit: Who’s coming with me!??!!? It’s going better. Stay tuned for a series on my todo spec.

Finally, thank you to all those in my life who helped me learn the things I know. I am self-motivated, but my knowledge is because of the people in my life.