I'm still undecided about accepting unicode on input as opposed
to latex-style input (e.g. \pi vs the unicode pi character).
The logic syntax would really benefit from using things like
\forall as a unicode character on input.
It makes the math I/O much prettier but it makes parsing
much harder.
The new Sane compiler is also being tested with the Fricas
algebra code. The compiler knows about the language but
does not depend on the algebra library (so far). It should be
possible, by design, to load different algebra towers.
In particular, one idea is to support the "tiny theories"
algebra