Skip to content

Latest commit

 

History

History
61 lines (45 loc) · 2.34 KB

design-principles.md

File metadata and controls

61 lines (45 loc) · 2.34 KB
Raw

Design principles

  • Quint should not annoy us:

    If a language concept has "standard" syntax in the mainstream languages, we adopt the mainstream syntax.

  • Quint should be easy to read:

    • In contrast to TLA+, it keeps the set of ASCII control characters to minimum.
    • It eliminates ambiguity in several operators (of tuples, records, sequences).
    • It allows the user to specify types, if needed.

  • Quint should be easy to write:

    • It uses a small set of syntactic rules.
    • Most of the operators are mnemonic.
    • Rarely used operators (e.g. temporal operators) are mnemonic.
    • Constants, variables, and operators may be annotated with types, to get quick feedback from the type checker.
    • Well-known operators are written like in the most programming languages. Several examples:
      • == instead of just =,
      • != instead of /= and #,
      • & and and instead of /\,
      • | and or instead of \/,
      • not instead of ~,
      • implies instead of =>,
      • / instead of \div,
      • . instead of ! when accessing a name in an instance.

  • Quint should be easy to parse:

    • It uses a small set of syntactic rules (its ANTLR4 grammar is 225 SLOC).
    • It borrows the best practices from the programming languages.
    • It should eliminate ambiguity in all operators and idioms.

  • Quint should be easy to pretty print:

    • Indentation is encouraged but not required.

  • Quint should be compatible with TLA+:

    • We keep one-to-one correspondence with the most of TLA+ operators.
    • There will be a transpiler to TLA+, so you can always jump back to TLA+.

  • Quint minimizes pain points of TLA+:

    • There is a clean separation between expressions of different modes: stateless, state, action, and temporal.
    • Updates to state variables are labelled as assignments: x' = e.
    • Recursive operators and functions are removed in favor of well-known concepts such as filter, map, and fold.
    • Module imports and instances in Quint look similar to state-of-the-art programming languages.

  • Quint is CLI-first:

    • The users should be able to parse and transpile Quint in the command-line.
    • The intermediate transpiler outputs are available in JSON.
    • IDE support (such as a VSCode plugin) is a beautiful opt-in, not a requirement.