Creatively Misusing TLA+

Even the general constraint solver? There are tools like Z3 which are designed to solve this sort of problem (quickly and exhaustively), and then there are tools like TLA+ which can solve this sort of problem (slowly and exhaustively).

Re: Creatively Misusing TLA+

#5

Post by vichu » Sun, Feb 12, 2023, 4:26 PM UTC

xrayarx wrote: post #3

Already posted https://news.ycombinator.com/item?id=34694123

This looks like a second-chance pool story as it didn't get much attention last time it was posted.

See dang's comments on the pool here: https://news.ycombinator.com/item?id=26998308

Re: Creatively Misusing TLA+

#6

Post by hwayne » Sun, Feb 12, 2023, 4:54 PM UTC

zeckalpha wrote: post #2

These all seem like good and reasonable uses rather than misuses to me.

"Creative misuse" refers to intended use. TLA+ isn't "meant" for these things, it just happens to be good for some (and kinda-okay for others). But that's the beauty of tools: it doesn't matter what they were designed to do, you can use them for whatever you need them to do.

It's harder to find creative misuses for programming languages because they're "intended" be general purpose. They're more like a material than a tool.

Re: Creatively Misusing TLA+

#7

Post by user5678 » Sun, Feb 12, 2023, 5:03 PM UTC

hwayne wrote: post #6

zeckalpha wrote: post #2

These all seem like good and reasonable uses rather than misuses to me.

"Creative misuse" refers to intended use. TLA+ isn't "meant" for these things, it just happens to be good for some (and kinda-okay for others). But that's the beauty of tools: it doesn't matter what they were designed to do, you can use them for whatever you need them to do. It's harder to find creative misuses for programming languages because they're "intended" be general purpose. They're more like a material than…

[dead]

Re: Creatively Misusing TLA+

#8

Post by sbierwagen » Sun, Feb 12, 2023, 6:56 PM UTC

vichu wrote: post #5

xrayarx wrote: post #3

Already posted https://news.ycombinator.com/item?id=34694123

This looks like a second-chance pool story as it didn't get much attention last time it was posted. See dang's comments on the pool here: https://news.ycombinator.com/item?id=26998308

I once left a comment on a submission that seemed to go through the second chance pool twice before getting traction, picking up three sets of replies each 24 hours apart.

Re: Creatively Misusing TLA+

#9

Post by Bjartr » Mon, Feb 13, 2023, 2:09 PM UTC

zeckalpha wrote: post #2

These all seem like good and reasonable uses rather than misuses to me.

It's a misuse in the same way using a flathead screwdriver to pry something open is a misuse. It may be a reasonable way to get the job done, but it's not what a screwdriver is designed for.