Going off of the example on the home page, the language reminds me a lot of Alloy, a model checking language. Alloy lets you describe facts about some discrete system and check for the existence (or nonexistence) of properties within those systems. If you expect some property to hold and it doesn't, Alloy will automatically produce a counter-example for you. Here's an example of a program modeling a file system:

  sig FSObject { parent: lone Dir }
  sig Dir extends FSObject { contents: set FSObject }
  sig File extends FSObject { }

  // A directory is the parent of its contents
  fact { all d: Dir, o: d.contents | o.parent = d }

  // All file system objects are either files or directories
  fact { File + Dir = FSObject }

  // There exists a root
  one sig Root extends Dir { } { no parent }

  // File system is connected
  fact { FSObject in Root.*contents }

  // Every fs object is in at most one directory
  assert oneLocation { all o: FSObject | lone d: Dir | o in d.contents }

I initially thought these model checking languages were purely academic in nature. But then a curious problem came up when I was working at AWS where folks were complaining that IAM policies generated by our library were sometimes growing to be too large in size (usually the limit was a few KB) - often due to redundant statements.

To solve this, a coworker implemented some code for merging IAM policies -- though the merging processe wasn't trivial because IAM policies can have both "Resources" and "NotResources", "Actions" and "NotActions", "Principals" and "NotPrincipals" etc. So to prove the algorithm was correct, he wrote up a short Alloy specification[1] (roughly mapping to the library code) that proved if two policy statements were merged, it wouldn't change the security posture. As a new engineer to the team, I'll just say that it blew my mind that this was possible -- actually using proofs to achieve goals in industry.

Needless to say, I'm curious to dive into Quint's differences and what kinds of models/specifications it excels with.

[1] https://github.com/aws/aws-cdk/blob/main/packages/aws-cdk-li...