In general, I think our short-term goal should be to make Provit a great place
for developing and using Formality apps. As we add features, Provit will slowly
become what we call Moonad.

- Give names and define the scope of each project and its desired features
  (Provit, Forall, Monad, FPM, etc.)

- Documentation on Provit should be as good as ReadTheDocs. How do we
  accomplish that? Multi-line comments? Markdown? Should we have a menu with
  the file tree?

- Posting and replying "normal posts" should be as intuitive as Reddit
  (should we have both a reply and an edit buttons? should replying import the
  active file?)

- What to do with citation flood? Rank? Using Ether, Upvotes?

- Bounties. Should we have them on Provit? How? Current plan is to have a
  smart-contract holding the Ether, and implement ta type-checking oracle,
  with future plans of implementing fm-core.js on the EVM.

- Apps inside Provit! This is pretty well-defined, but must be developed by
  someone (probably me). Requires some Formality code for effect monads and
  some JS code for the renderiing / IO.

- Accounts. We need implementation of authentication on the site, and a
  matching implementation on Formality. How will that be done? ECDSA? Just
  Ethereum accounts?

- FPM needs to accept only well-typed terms, and it must have a proper
  database. This must be developed with caution, since type-checking can be
  very costly, so perhaps an architecture where we cluster of async
  type-checking workers that do not block the main server?

- FPM namespacing and mutability. Do we keep it as is? Right now I think: yes,
  I believe our system of unique, eternal, immutable names is amazing and
  should stay. Just accept that we can't change the "landing page" of something
  like `Algebra@0`, which is perhaps a good thing, actually.

- What else?