Hillel Wayne

> Besides, I don't see anybody actually claiming "Formal Verification is a great way to write software. We should prove all of our code correct.", I was the one saying...

Anyway thinking of the best way to transparently retire it

We enter the hot state when we add a new pending request and only leave it when `sizeof(pendingWDReqs) == 0`. Now consider the following sequence of states for `pendingWDReqs`: ```...

I could probably whip up a css to do this, ugh css

I don't know how to spell arithmetic

Thanks for bringing this up! I think the unclear bit is here: > In the prior task example, `assignments` was always a function in the function set `[Tasks -> SUBSET...

Technically it's a specification of an algorithm, in the broad sense of the word "algorithm". Are you asking me to define a specification more clearly?

Hi, Sorry I'm getting to this late! Only saw this just now. When you do `java -cp tla2tools.jar pcal.trans`, it will clobber your existing `scratch.cfg` file, meaning the invariant is...

I teach my classes in VSCode, the problem that keeps me from migrarting everything (besides laziness) is that you can't put negative numbers or sequences as constants in VScode, at...

The problem isn't with VSCode, it's with TLC. TLC's `.cfg` format can't accept anything besides basics numbers and sets. To make constants with sequences or negative numbers, you need to...