soonad / formalityfm Goto Github PK

Newbie here. I'm impressed by the goals (and their actual current state of implementation). Well done!

I'd like to ask some questions (some more dumb, some hopefully less). I might be adding more over time in comments below 😉.

1. Do you have plans to make the syntax even simpler? I mean e.g. removing unnecessary colons, arrows, etc. Feel free to get inspired by the highly readable but very minimal syntax of V or (a bit less) Arturo.
2. What's the license of the code? If not decided, I'd raise my hand for MIT or BSD or any OSI-approved (unlike FSF-approved) license.
3. Having a C backend along with JS backend is a win-win nowadays. Would you consider adding a C backend? It might attract new contributors (namely those not afraid of low-level interfaces, etc.). And exactly these "low-level" thinking contributors are especially important in this phase of development IMHO.
4. As follow-up of (3) - have you considered the trick above-mentioned language V uses regarding compiler backends? Namely for debug purposes use TCC for sub-second compile&run and then some proper (GCC, Clang, MSVC, ...) compiler for -prod build?
5. Another follow-up on (3) - do you think making a generic C FFI abstraction would be possible in Formality? This is IMHO necessary for interfacing with "existing impure world" to allow Formality to be used immediately without re-introducing and re-programming everything by hand again.
   1. This might require something like claim similar to what I envisioned in zesterer/tao#8 (comment) (as a substitute for C libs being incapable to deliver the proof terms Formality requires) along with effect from Koka to cleanly handle the "errors" and all other impure stuff.
6. Speaking of errors in (5), it's inevitable for a practical language to gracefully (here I mean really only visually syntactically) handle any non-default code branch. I dislike C++/Java/... exceptions, I dislike (but less) optionals, I dislike goto, I dislike pure functions (because the number of arguments becomes tremendously verbose), but I think the effect as in Koka (or the same but slightly disguised in Dylan as outlined in henrystanley/Quark#2 (comment) ) might have some potential (compared to rewriting the whole lib in Formality).
7. How to write mocked up or incomplete code to "just demonstrate a default path" in Formality without thinking about the proper types? This is again a practicality question (boiling down to the proposal of sassert assert and claim from zesterer/tao#8 (comment) which can be added any time later to make the code type check without rewriting & refactoring huge portions of the code).