On: Learn TLA+ (2018)

[strangecasts]

Specifications aren't tied to any specific programming language - you're outlining how the algorithm should work, not the implementation.

(You can write Java code and invoke it during model-checking if you really need to, but I haven't come across any situation where it's actually necessary.)

[k__ → strangecasts]

Ah, okay.

I had the impression it was about somehow writing a program in a more strict language and then exporting it to Java.

I don't do much algorithmic design.