Improvements to F*: Brainstorm 2019

Performance

Profiling tools for F* / OCaml?
Memoization of typechecking (Guido, Aseem, Nik ... See Memoizing-typechecking and Notes-on-optimizations-for-type-inference-and-memoization)
Making NBE more mainstream
Measuring performance more systematically, CI performance reports etc.

Context pollution
- Using Aseem's opaqueness recipes (e.g. Style 2, hiding via indirection, from this note is already implemented in EverCrypt)
- Canaries: Simple proofs from Sequences, Buffers, Modifies, etc. attempted in larger proof contexts
Interacting with top-level proofs are much easier than with proofs in some nested scope
Comprehensive review of SMT patterns in sequence, buffer, modifies etc.

The main long-range effort we have on improving Low* programming is the DSLs for stateful programming work with Zoe
What else could we be doing, aside from incremental library improvements etc.

Nesting tactic splitting at arbitrary depth: e.g., synthesizing terms with an assert p by t and then discharging p by spawning a tactic process for t to solve p.
"where" clauses for tactics: i.e., within a nested scope, being able to say assert p by t ... and later where t = .... Would allow interacting with nested assertions at the top level.
How to make Meta-F* more suitable for routine use and small scale proofs?
- Solve the context pollution problem for FStar.Tactics
- See https://github.com/FStarLang/FStar/issues/1419
- Even simply uses of apply tactics can be very painful
- ... ?

Double indirection problem in symbol lookup: i.e., need to launch an F* process each time you want to follow the definition of a symbol across a module
"process is busy": Handling concurrent requests in the F* server?

fstarlib vs fstartaclib packaging
More incrementality/parallelism in building OCaml
Fine-grained statistics on time spent in the typechecker, time spent in Z3, etc. to identify performance regressions