Zoncolan and SPARTA both use abstract interpretation at their core, but as far as the code/implementation goes they are mostly unrelated. Zoncolan is built on top of the Hack type checker (https://hacklang.org/), which means that it's largely written in OCaml.
I think (2) is the overriding concern: we're getting really great results with the static analysis tools we've built internally on top of the Hack type checker. Building a similar tool on top of mypy would've required fairly invasive changes; we decided to use the Hack type checker infra instead.
Full disclosure: I worked on the Hack type checker briefly, a long time ago :)
You can run Pyre without using watchman if your editor-of-choice supports LSP -- the two modes are basically complementary. You can also run `pyre check` in non-incremental mode, though that may be slower depending on the size of your codebase.
Good question [I am the 'Pieter' on that blog post]. There will be a talk at PyCon that covers parts of this. It comes down to two reasons:
1) Performance. We needed something that would consistently work quickly on Instagram's server codebase (currently at several million lines).
2) We are building deeper semantic static analysis tools on top of Pyre. We've built some of these tools for Hack/PHP already, so following the Hack type checker's architecture is the best way for us to achieve this.