Why would someone use this instead of, say, TLA+ or Alloy?
TLA+ is already an "extremely lightweight specification language", with a super-useful model checker, and a ton of tooling around it (e.g. VSCode plugin), books, talks, hundreds of battle-tested examples online, etc.
The Github page[0] has some more "why" info. I think this is the crux of it:
> There's a possibility for something with a much lower barrier to entry [...] than something like Z. Part of what makes this possible is that we can jettison a formal semantics entirely. It doesn't need to mean anything. At the end of the day the only semantics will be in the mind of the human reader.
So, it can't really be "machine-checkable" like TLA+ or Alloy are, because the symbols don't mean anything. I take it that's it's supposed to be more of an aid to thought, like diagramming on a whiteboard.
For one thing, the fact that Pantagruel shows spec examples right on the homepage is very nice. Being familiar with neither tool, I just clicked around the TLA+ homepage and could find no actual spec examples - at best is a link to a zip which supposedly has a start.pdf file in it.
TLA+ might be a better language, but with no prior horse in the race the better-described tool will be my first to try. And unless there is a showstopper issue, I'd likely stick with it.
erichocean|4 years ago
TLA+ is already an "extremely lightweight specification language", with a super-useful model checker, and a ton of tooling around it (e.g. VSCode plugin), books, talks, hundreds of battle-tested examples online, etc.
Taikonerd|4 years ago
> There's a possibility for something with a much lower barrier to entry [...] than something like Z. Part of what makes this possible is that we can jettison a formal semantics entirely. It doesn't need to mean anything. At the end of the day the only semantics will be in the mind of the human reader.
So, it can't really be "machine-checkable" like TLA+ or Alloy are, because the symbols don't mean anything. I take it that's it's supposed to be more of an aid to thought, like diagramming on a whiteboard.
[0] https://github.com/subsetpark/pantagruel
dotancohen|4 years ago
TLA+ might be a better language, but with no prior horse in the race the better-described tool will be my first to try. And unless there is a showstopper issue, I'd likely stick with it.
hwayne|4 years ago