I find this really interesting. The theoretical basis of the language and type theory seems sound on a brief inspection and the implementation also seems to have taken great steps toward a 'friendly' syntax with convenience features ready to be used. I am wondering if anyone with more familiarity with the implementation knows where they are handling (or if they are) proof-irrelevance and erasure issues? The language seems pretty 'flat' at the type level (no explicit Universes), but clearly with the emphasis on proof solving the theory can not be Type:Type.
TL;DR -- I think the language looks nice, and the compile to JS (from what I read of the Formcore source) looks to be well done. Also, the docs that are present are well presented in a non-academic way that I find pretty readable.
TL;DR -- I think the language looks nice, and the compile to JS (from what I read of the Formcore source) looks to be well done. Also, the docs that are present are well presented in a non-academic way that I find pretty readable.