write

@@ -7,7 +7,7 @@ There have been a number of blog posts related to Polonius as it evolves:
- [Polonius and the case of the hereditary harrop predicate](https://smallcultfollowing.com/babysteps/blog/2019/01/21/hereditary-harrop-region-constraints/)
- ... TODO add the rest ...

[polonius-proof](https://github.com/lengyijun/polonius-proof/) uses theorem prover to prove that `naive` and `datafrog-opt` generate same error.
[polonius-proof](https://github.com/lengyijun/polonius-proof/) uses a theorem prover to prove that the `naive` and `datafrog-opt` variants generate the same errors.

The academic work "Oxide" is partially inspired by Polonius: