quint
quint copied to clipboard
informalsystems
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Our "Hello, World!" tutorial is a tutorial on how to specify a hello world program rather than a "hello world" for writing specs in quin. We can make more gentle...
Apparently this will fix #428
We now have different kinds of sets, including `Int` and `Nat`, and sets containing them. We should update `isFinite` to work correctly.
We don't have any setup for property-based testing. Pointed out by @shonfeder at https://github.com/informalsystems/tnt/pull/81/files#r853271142. I can see that helping a lot with testing since writing unit tests for individual IR...
As discussed in #386 - https://github.com/informalsystems/tnt/pull/386#discussion_r1039485690 - https://github.com/informalsystems/tnt/pull/386#discussion_r1039482799 We have several builtin operators which should be simple to define as part of our standard library instead. E.g., - `notin` -...
It would be nice to have test coverage reports on PRs since the early days of this project so we don't have to get back to old files to add...
Linter should be one of the transpiler's tasks. See [ADR001](https://github.com/informalsystems/tnt/blob/main/doc/adr001-transpiler-architecture.md) for the architecture. We could use the architecture of [eslint](https://eslint.org/) as an inspiration. Most likely, this task requires and ADR.
@hvanz has reported that type checking is noticeably slower when using sum types. Some increased complexity is to be expected given the implementation, but we don't want it to reduce...
Required for #388 This will really help with knowledge sharing of common idioms and help us help users to opt for best practices when describing common computations.
Suggested in https://github.com/informalsystems/quint/pull/1005#issuecomment-1630926781
Metadata
Owner
Metadata
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)