Add tutorial (refinement type checking) (#88)

HarvardPL · Oct 11, 2024 · c4752db · c4752db
1 parent cc91966
commit c4752db
Show file tree

Hide file tree

Showing 12 changed files with 1,225 additions and 7 deletions.
diff --git a/README.md b/README.md
@@ -2,7 +2,21 @@
 
 ![Build Status](https://github.com/HarvardPL/formulog/actions/workflows/maven.yml/badge.svg)
 
-Datalog with support for SMT queries and first-order functional programming.
+**TL;DR: write SMT-based program analyses (symbolic executors, refinement type checkers, etc.) in an optimized Datalog-like language.**
+
+Datalog has proven to be a useful language for implementing a range of program analyses, but analyses that use SMT-solving cannot be easily written in traditional versions of Datalog.
+Formulog sets out to fill this gap by augmenting Datalog with ways to construct and reason about SMT formulas, as well as some first-order functional programming to make life easier.
+
+**Why write your SMT-based analysis in Formulog?**
+
+1. By combining logic programming, functional programming, and SMT solving, Formulog makes it possible to encode many analyses declaratively at the level of mathematical specification (e.g., inference rules), closing the gap between specification and implementation---and often revealing bugs in the spec!
+2. This high-level encoding makes it possible for Formulog to apply high-level optimizations to your analysis, like automatic parallelization and goal-directed evaluation.
+3. Thanks to our [Formulog-to-Soufflé compiler](#compiling-formulog-programs), you can automatically generate a C++ version of the analysis that leverages highly optimized Datalog algorithms and data structures.
+
+**Interested?**
+To get a sense for what's involved in building a nontrivial SMT-based analysis in Formulog,
+check out our [tutorial](./docs/tutorial/tutorial.md) on implementing a refinement type checker in Formulog.
+For more tips on where to start, check out the section on [writing Formulog programs](#writing-formulog-programs) later in this document.
 
 ## Setup
 
@@ -299,18 +313,24 @@ $ ./build/flg --dump-idb
 
 ## Writing Formulog programs
 
-See the documentation in `docs/`. Some shortish example programs can be found in
-the `examples/` directory. To see an example of a larger development, check out
-our implementation of
-a [type checker for Dminor](https://github.com/HarvardPL/dminor-in-formulog), a
-language built around refinement types.
+Check out our [tutorial](./docs/tutorial/tutorial.md) for a walk-through of how to encode a refinement type system in Formulog.
+Additional shortish example programs can be found in the [examples](./examples) directory.
+For examples of larger developments, see the case studies we have used in publications:
+
+- [a refinement type checker](https://github.com/aaronbembenek/making-formulog-fast/blob/main/benchmarks/dminor/bench.flg)
+- [a bottom-up points-to analysis for Java](https://github.com/aaronbembenek/making-formulog-fast/blob/main/benchmarks/scuba/bench.flg)
+- [a symbolic executor an LLVM fragment](https://github.com/aaronbembenek/making-formulog-fast/blob/main/benchmarks/symex/bench.flg)
+
+See the [language reference](./docs/00_language_ref.md) for details about Formulog constructs.
 
 Syntax highlighting is available for Visual Studio Code (follow instructions [here](https://github.com/HarvardPL/formulog-syntax)) and Vim (install [misc/flg.vim](./misc/flg.vim)).
 
+Finally, please raise a [GitHub issue](https://github.com/HarvardPL/formulog/issues/new) if you want to try out Formulog but need additional information/assistance---we're happy to help! :)
+
 ## Contributing
 
 Contributions to this project are most welcome!
-Please open a [GitHub issue](https://github.com/HarvardPL/formulog/issues) and then link a pull request to it.
+Please open a [GitHub issue](https://github.com/HarvardPL/formulog/issues/new) and then link a pull request to it.
 Pull requests must be in the [Google Java format](https://github.com/google/google-java-format) before being merged.
 To reformat your code, run `mvn spotless:apply`; you can also check if your code is conformant (without reformatting it) by running `mvn spotless:check`.
 

diff --git a/docs/00_language_ref.md b/docs/00_language_ref.md
@@ -0,0 +1,13 @@
+# Formulog Language Reference
+
+This set of documents describes the Formulog language.
+Please raise a [GitHub issue](https://github.com/HarvardPL/formulog/issues/new) if anything is unclear, incomplete, or incorrect :)
+
+For an overview of Formulog and its motivations, we recommend checking out our [OOPLSA'20 paper](https://aaronbembenek.github.io/papers/formulog-oopsla2020.pdf).
+
+## TOC
+
+1. [Language basics](./01_language_basics.md)
+2. [Program safety](./02_program_safety.md)
+3. [Goal-directed evaluation](./03_goal_directed_evaluation.md)
+4. [Logical formulas](./04_logical_formulas.md)
diff --git a/docs/tutorial/images/figure_2_1.png b/docs/tutorial/images/figure_2_1.png
diff --git a/docs/tutorial/images/figure_3_1.png b/docs/tutorial/images/figure_3_1.png
diff --git a/docs/tutorial/images/figure_3_2.png b/docs/tutorial/images/figure_3_2.png
diff --git a/docs/tutorial/images/figure_3_3.png b/docs/tutorial/images/figure_3_3.png
diff --git a/docs/tutorial/images/figure_3_4.png b/docs/tutorial/images/figure_3_4.png
diff --git a/docs/tutorial/images/figure_3_5.png b/docs/tutorial/images/figure_3_5.png
diff --git a/docs/tutorial/images/figure_3_6.png b/docs/tutorial/images/figure_3_6.png
diff --git a/docs/tutorial/images/section_3_3_1.png b/docs/tutorial/images/section_3_3_1.png