Add several FAQ entries on comparisons #1506

bugarela · 2024-09-17T15:22:22Z

Hello

These adds a bunch of FAQ entries for questions like "How does Quint compare to X"? to our website FAQ.

bugarela · 2024-09-17T15:26:08Z

Hi @p-offtermatt @romac @ivan-gavran ! Tagging you here as you might have good opinions on these. Review is totally optional, but I'd definitely appreciate them ❤️

docs/pages/docs/faq.mdx

ebuchman

This is great! Maybe as I final thing we should have a "So, what should I use Quint for" that just summarizes like

if you can do static analysis on your code, do it
if you need a full mathematical proof, use Lean etc.
if you need a full mathematical proof thats also executable code, use Idris etc.
if you need a model of your system you can play with to improve your understanding of the protocol and check certain properties, use Quint

or something like that

I think overall highlighting that with Quint its much easier to check invariants on protocols than formally proving it all with an assistant would be helpful

docs/pages/docs/faq.mdx

ebuchman · 2024-09-17T22:19:27Z

docs/pages/docs/faq.mdx

+
+Proof assistants require you to write deductive proofs, while model checkers (as
+in Quint), use an inductive approach, exploring all reachable states in a model.
+Proof assistants are mostly used for research, and model checking techniques are


don't really critical systems get proven though?

and isn't a lot of focus in like cryptography and ethereum on using proof assistants? we may want to add something to that effect.

would be great for each to add some examples of where they have been used successfully to also ground the comparison

From what I gathered, the meaningful industry use cases is like years of work from several experts. I'll try to find concrete information and add some "they did this but it took this big effort/expertise". In general, CompCert is the biggest example. For ethereum stuff, I need to check how many things are actually done (as opposed to ongoing research).

I looked through a lot of Veridise's public audit reports. I found one from a while ago where they used coq to verify a zk circuit https://veridise.com/wp-content/uploads/2023/09/VAR-RLN.pdf

also this https://veridise.com/wp-content/uploads/2023/08/VAR-Unirep.pdf

one more: MatterLabs verifying the zk-verifier https://eprint.iacr.org/2024/768.pdf

Cool, thanks! Will add those and look for more

Co-authored-by: Ethan Buchman <[email protected]>

p-offtermatt

Nice, I think these are useful. Left a few comments

p-offtermatt · 2024-09-18T07:33:29Z

docs/pages/docs/faq.mdx

+   proof system (TLAPS), while Quint doesn't. Therefore, it is possible to write
+   more advanced formulas in TLA+ than in Quint, even ones that are not
+   supported by the existing model checkers, and then prove them using the proof
+   system. Quint restricts you to a fragment of TLA with the intention of


Suggested change

system. Quint restricts you to a fragment of TLA with the intention of

system. Quint restricts you to a fragment of TLA+ with the intention of

Not sure whether this is TLA on purpose or its missing the +

I guess both the language and the logic could make sense here

Yeah, it was on purpose. Both make sense, right. I just figure it is easier to explain to people that both Quint and TLA+ are based on TLA (although both add ZFC on top of TLA, so there is actually more that is shared).

I think saying TLA+ in this sentence would be incorrect. Quint is not based on TLA+ the spec language, but on TLA the logic.

In this sense, you are correct. But also, I've seen TLA+ described as:

The “+” in TLA+ uses a formal set theory based on ZFC to allow TLA variables to take on many kinds of values (atoms like numbers and strings, finite and infinite sequences, sets, records, and functions).

in some places before (I think Lamport wrote this). And since Quint also has ZFC tihngs, I think it is also right to say it is a fragment of TLA+

That's right. Probably it's better to say "Quint restricts you to a fragment of the underlying logic of TLA+". The underlying logic of TLA+ is TLA plus a variant of ZFC. The "+" also adds non-logical constructs such as modules.

p-offtermatt · 2024-09-18T07:35:47Z

docs/pages/docs/faq.mdx

+   supported by the existing model checkers, and then prove them using the proof
+   system. Quint restricts you to a fragment of TLA with the intention of
+   preventing unintentional usage of operators that lead to complicated
+   behaviors that are hard to debug and understand. Our understanding is that


I don't like the last sentence so much and would reformulate, but up to you. Isn't the distinction more about Quint wanting to avoid things that "accidentally" blow up the state space, when they could instead be written in a way that is nicer for the size of the state space?

Hmmm I don't think we can attribute state space management to the constraints of Quint. What I have in mind here is that in TLA+ you can write x = x' for x' = x, which is exactly the same in terms of state space, but more complex to understand if you are not thinking about math. Then, there are the weirder ones like (x + 1)' = x and f'(x') etc, and the ones which would actually affect the search space as x' > x.

But, mostly, we are just trying to avoid people using the prime operator in different ways as it is not obvious what it would do, and people might expect something different from what it actually means. This also happens with non determinism.

My sentence comes from me believing that people who are more used to math than to programming will like TLA+ better than Quint (at least for the syntax, and they might even be not that bothered by the tooling). A good rule of thumb might be: would you rather read a map like { f(x) : x ∈ S } or S.map(x => f(x))? I can read both fine, but I prefer the second one by far. But there are definitely people who prefer the first.

docs/pages/docs/faq.mdx

p-offtermatt · 2024-09-18T07:52:42Z

docs/pages/docs/faq.mdx

+
+Proof assistants require you to write deductive proofs, while model checkers (as
+in Quint), use an inductive approach, exploring all reachable states in a model.
+Proof assistants are mostly used for research, and model checking techniques are


I looked through a lot of Veridise's public audit reports. I found one from a while ago where they used coq to verify a zk circuit https://veridise.com/wp-content/uploads/2023/09/VAR-RLN.pdf

p-offtermatt · 2024-09-18T07:54:47Z

docs/pages/docs/faq.mdx

+
+Proof assistants require you to write deductive proofs, while model checkers (as
+in Quint), use an inductive approach, exploring all reachable states in a model.
+Proof assistants are mostly used for research, and model checking techniques are


also this https://veridise.com/wp-content/uploads/2023/08/VAR-Unirep.pdf

docs/pages/docs/faq.mdx

p-offtermatt · 2024-09-18T08:00:56Z

docs/pages/docs/faq.mdx

+Quint is used to reason about behaviors of programs and how things change over
+time. If you can use a static analyzer to search for a class of errors (i.e.
+null checks), you should definitely use that. Use Quint for what you cannot do
+with a static analyzer (which is a lot!).
+
+This is also one of the reasons why Quint has a type system. Although we could
+check typing using invariants, as people often do in TLA+, we can do it
+statically with a regular type checker - and that is much better.
+
+Static analyzers won't be able to tell you if your consensus algorithm does
+consensus as you expect, but Quint will.


I think this one should explain a bit more what static analyzers can be used for and what they cannot - I think it needs a one sentence explanation at the start that lays out what static analyzers even are, on a very high level

Co-authored-by: Philip Offtermatt <[email protected]>

hvanz · 2024-09-18T14:59:45Z

docs/pages/docs/faq.mdx

+
+Proving something using one of these tools provides a much stronger guarantee
+than verifying something with a model checker. Proofs derive directly from
+constructive mathematics, while model checkers are complex implementations on


Be careful with the expression "constructive mathematics" (https://plato.stanford.edu/entries/mathematics-constructive/).

The logic of Isabelle/HOL is not constructive. ~~I think Lean supports some form of constructive logic but I'm not sure~~. "Lean is based on a version of dependent type theory known as the Calculus of Constructions." Only Coq is constructive with its Calculus of Inductive Constructions.

Oh, my bad! I thought all of them were used constructive logics. Do you have any suggestions on what would be more accurate here? I just want to say that there is a really low chance that there is an implementation error on the proof assistants that would result in wrong proofs being checked, while there is much more room for mistakes in model checker implementations.

Proof assistants are software and thus can have bugs too. They are generally more trustworthy than model checkers because these proof assistants in particular rely on a small kernel implementing the core logical rules. All proofs reduce to the rules in the kernel. The kernel is very small, probably a few hundred lines of code, so it's easier to check and trust that it faithfully implement the rules.

That's good, thanks!

bugarela · 2024-10-03T14:00:31Z

Thank you for all the comments! I believe I addressed all of them and it looks much more solid :)

Add several FAQ entries on comparisons

e9d55ea

bugarela requested review from romac, p-offtermatt, MahtabNorouzi and ivan-gavran September 17, 2024 15:24

ebuchman reviewed Sep 17, 2024

View reviewed changes

docs/pages/docs/faq.mdx Outdated Show resolved Hide resolved

Update docs/pages/docs/faq.mdx

a87a4b2

ebuchman approved these changes Sep 17, 2024

View reviewed changes

Update docs/pages/docs/faq.mdx

9e37983

Co-authored-by: Ethan Buchman <[email protected]>

p-offtermatt reviewed Sep 18, 2024

View reviewed changes

Apply suggestions from code review

4f74f25

Co-authored-by: Philip Offtermatt <[email protected]>

hvanz reviewed Sep 18, 2024

View reviewed changes

bugarela added 5 commits September 19, 2024 11:44

Mention usages of Coq in industry

ecd2237

Improve section on why proof assistants have stronger guarantees

c3363a2

Improve FAQBox component to have nice anchors

7a7076f

Explain static analyzers

c87df37

Merge branch 'main' into gabriela/faq-comparissons

2d2d455

bugarela enabled auto-merge October 3, 2024 14:00

bugarela merged commit 2a355b2 into main Oct 3, 2024
14 checks passed

bugarela deleted the gabriela/faq-comparissons branch October 3, 2024 14:04

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add several FAQ entries on comparisons #1506

Add several FAQ entries on comparisons #1506

bugarela commented Sep 17, 2024

bugarela commented Sep 17, 2024

ebuchman left a comment

ebuchman Sep 17, 2024

bugarela Sep 17, 2024

p-offtermatt Sep 18, 2024

p-offtermatt Sep 18, 2024

p-offtermatt Sep 18, 2024

bugarela Sep 18, 2024

p-offtermatt left a comment

p-offtermatt Sep 18, 2024

p-offtermatt Sep 18, 2024

bugarela Sep 18, 2024

hvanz Sep 18, 2024

bugarela Sep 19, 2024

hvanz Sep 19, 2024

p-offtermatt Sep 18, 2024

bugarela Sep 18, 2024

p-offtermatt Sep 18, 2024

p-offtermatt Sep 18, 2024

p-offtermatt Sep 18, 2024

hvanz Sep 18, 2024 •

edited

Loading

bugarela Sep 19, 2024

hvanz Sep 19, 2024

bugarela Sep 19, 2024

bugarela commented Oct 3, 2024

	system. Quint restricts you to a fragment of TLA with the intention of
	system. Quint restricts you to a fragment of TLA+ with the intention of

Add several FAQ entries on comparisons #1506

Add several FAQ entries on comparisons #1506

Conversation

bugarela commented Sep 17, 2024

bugarela commented Sep 17, 2024

ebuchman left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

p-offtermatt left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hvanz Sep 18, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bugarela commented Oct 3, 2024

hvanz Sep 18, 2024 •

edited

Loading