Andrew Helwer on Nostr: Playing around with the snowcat type checker for TLA+ for the first time and I really ...
Playing around with the snowcat type checker for TLA+ for the first time and I really like it! Other than some awkwardness about having to explicitly transform functions-as-sequences, it completely matches up with the model I have in my head as I write TLA+. I will use it when I write my next specification.
#tlaplus
Published at
2024-02-01 21:13:53Event JSON
{
"id": "7b209e0026b221dd0bb105a118f0022354b261db09db3520f6af038f8ddfc3b4",
"pubkey": "6235fe36d733665c235dbec5983d768400cdb414ea18e0633cfe9d9c1ac6b02d",
"created_at": 1706822033,
"kind": 1,
"tags": [
[
"t",
"tlaplus"
],
[
"proxy",
"https://fosstodon.org/users/ahelwer/statuses/111858288814225484",
"activitypub"
]
],
"content": "Playing around with the snowcat type checker for TLA+ for the first time and I really like it! Other than some awkwardness about having to explicitly transform functions-as-sequences, it completely matches up with the model I have in my head as I write TLA+. I will use it when I write my next specification.\n\n#tlaplus",
"sig": "2e4e6d4eaeb0cdbf1ca014e306d74780d2d24adeffc6ac8b7582273a52addbb47a884716b0f52d8eb0f392749b31891b0314b21fa1970208b761202337984c36"
}
