At home trying to put together thoughts for a post on how to get the most out of Slack without spending all day looking at it.
At work shepherding discussions on how things should be in a philosophical sense and then we can start to work towards those goals in code.
Try as I may, I just cannot get my head around how to think in order to produce specs in PlusCal / TLA+. I really wish I could because I feel that it could yield enormous benefits for me & my colleagues at work, and of course it would be a handy tool to have in the toolbox for the future.
To start out, you can just think of it as a nice DSL for specifying a finite state machine. Every action defines a state transition, and unprimed variables are the guards - if they are true of the state you’re in then the transition can be taken. And the primed variables will be the values of your variables in the next state. Thinking of your program as a state machine is pretty powerful, and even intuitive for many people! Then you can define invariants that must stay true in every state, and the model checker can check that. Also all variables are global, which people find weird, until they realize how valuable a single consistent view of the entire system is for writing & checking invariants.
Once you start caring about liveness (good things eventually happen, checked with temporal properties) in addition to safety (bad things don’t happen, checked with invariants) you will have to augment your understanding beyond the state machine model. But 90% of people really only need and use safety checking, where the state machine mental model is all you need.
@hwayne made the website https://learntla.com (and your company can hire him to lead a workshop teaching you & your coworkers about the language!) and there is also a video course made by Leslie Lamport. Personally I learned from the book Specifying Systems but that was a decade ago and many things have been made since then: http://lamport.azurewebsites.net/tla/learning.html
I voted for a difficulty score of 1, the lowest possible, as it was a 10-minute task. However, my colleagues didn’t agree; they voted that my task was harder than it looked and worthy of several days of work.
Part of me
thinks wishes that there is a fair bit of embellishment in this article with the above quote as an example. But while this is not my experience, I realise that it is probably quite somewhat common place.
I was surprised to see builds for code in Sourcehut in the list of recent builds, given the plans for Sourcehut to block the Go module proxy. But I was glad to see  that Sourcehut and the Go crowd reached som amicable arrangement.
I’m on-call so hopefully that’ll be quiet. I am working on a development harness for local development so I might write a few lines there. And for proper work I’m a bit swamped with a deadline so I might sling some code up over the weekend, when there’s no meetings and fewer distractions.
Might play some Burnout Revenge on the PS2 as well.
Hopefully lots of refactoring (database operations in Go) that is if I can keep away from Slack and meetings!