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.

[0] https://github.com/subsetpark/pantagruel