Write an overview of liquid-fixpoint

[facundominguez]

The README says this much

This package implements a Horn-Clause/Logical Implication constraint solver used for various Liquid Types. The solver uses SMTLIB2 to implement an algorithm similar to: ...

which I think is not quite sufficient to get people excited about it. liquid-fixpoint caught me only after I learned about the PLE algorithm, and then REST, I do not understand elim as well, but I regard it essential to deal with abstract predicates in LH and inference of refinement predicates in general.

When I explain liquid-fixpoint to someone, I say it does three things:

1. It infers the refinement types of your program
2. It does the unfolding of functions in your constraints to prove them
3. It does the rewriting of your expressions using lemmas in the environment

I think these points, together with pointers to larger explanations, would be more compelling.

Ideally, I'd like to have a first defense of blogposts giving overviews for each algorithm, followed by a second defense with the academic publications. We already have the publications. Perhaps we have some of the blogposts too and we just need to put it all together, or perhaps there is some more writing to do.

[ranjitjhala]

Yes it’s definitely “dry” — pretty sure we have blog post for all of those … let me try to dig up!

…

On Fri, Apr 8, 2022 at 10:54 AM Facundo Domínguez ***@***.***> wrote: The README says this much This package implements a Horn-Clause/Logical Implication constraint solver used for various Liquid Types. The solver uses SMTLIB2 to implement an algorithm similar to: ... which I think is not quite sufficient to get people exited about it. liquid-fixpoint caught me only after I learned about the PLE algorithm, and then REST, I do not understand elim as well, but it I regard it essential to deal with abstract predicates in LH and inference of refinement predicates in general. When I explain liquid-fixpoint to someone, I say it does three things: 1. It infers the refinement types of your program 2. It does the unfolding of functions in your constraints to prove them 3. It does the rewriting of your expressions using lemmas in the environment I think these points, together with pointers to larger explanations, would be more compelling. Ideally, I'd like to have a first defense of blogposts giving overviews for each algorithm, followed by a second defense with the academic publications. We already have the publications. Perhaps we have some of the blogposts too and we just need to put it all together, or perhaps there is some more writing to do. — Reply to this email directly, view it on GitHub <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_543&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=RtpDg-McLvNWVJ3br7sp9Lw9KYJFK_ZoQ4uSmh_ET6dgIAP-JKaEAx78w7hslT6C&s=-RD_thntAyMcg70JESqnl4Ampouk6Vrku65mhILKdLQ&e=>, or unsubscribe <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OH6NO2N3ZJ3GAPQXUTVEBXGTANCNFSM5S5HUVCA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=RtpDg-McLvNWVJ3br7sp9Lw9KYJFK_ZoQ4uSmh_ET6dgIAP-JKaEAx78w7hslT6C&s=Up1iT3FhFdE-cEpqwwcZ9Gejh3achvveXFp9j2lnEms&e=> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>