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

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-lib/aws-iam/docs/policy-merging.als https://github.com/aws/aws-cdk/blob/main/packages/aws-cdk-li...