Why?

Writing software is hard. From creating new algorithms to orchestrating distributed systems, many things can go wrong.

If you are a business person, Quint can be the tool to secure your new software idea before shipping it and avoid discovering bad edge cases through hackers.

If you are a programmer of any kind, Quint can be the tool to help you design and validate new solutions without taking the paranoia all by yourself. It can also help you optimize your solutions by answering the "can I do this?" questions for you. In the words (opens in a new tab) of Chris Newcombe, from Amazon Web Services:

PS: You might want to check FAQ entry: How does Quint compare to TLA+?

Formal methods are a big success at AWS, helping us prevent subtle but serious bugs from reaching production, bugs we would not have found through any other technique. They have helped us devise aggressive optimizations to complex algorithms without sacrificing quality. At the time of this writing, seven Amazon teams have used TLA+, all finding value in doing so, and more Amazon teams are starting to use it. Using TLA+ will improve both time-to-market and quality of our systems. Executive management actively encourages teams to write TLA+ specs for new features and other significant design changes. In annual planning, managers now allocate engineering time to TLA+.

So far, protocol designers have been the biggest fans of Quint. They have started using Quint as their new pen and paper to draft, and later validate, new designs. Quint has also been a good partner in complex software audits, and while onboarding and studying new algorithms.

If you are a civil engineer, you know that constructing buildings is hard, and that's why you spend so much time working on blueprints¹.

If you are a software engineer, you know that writing software is hard, and that's why you should learn Quint.