The author of ALT has a long burning desire to build a better spreadsheet for citizen developers. Just imagine a spreadsheet, but now with all the nice features that we care about as software developers!
ALT has almost all of the features available to make that dream become a reality.
However, the current implementation is not nearly efficient enough to be used by end users. Luckily, there are many performance improvements that can be considered:
- Exploit sorting/ordering to reduce indexing from
- Add specialized rewrite rules for common idioms
- Compile ALT programs
- Dynamically add indexes to frequently used data
- Dynamically decide on the best (internal) data structure for a value
- Incrementally re-compute only what is necessary
It would be very nice to have a formal specification of ALT’s (term rewriting) semantics in Coq or Isabelle/HOL. With such specification we could (hopefully!) prove that ALT has the global confluence property and that ALT terminates for all terms/programs (and most importantly, that programs with cycles always terminate). We could also use the formal specification to check whether certain rewrite rules are admissable, or prove little theorems.