Questions and future

[dumblob]

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 :wink:.

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 https://github.com/zesterer/tao/issues/8#issuecomment-707232679 (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 https://github.com/henrystanley/Quark/issues/2#issue-673131403 ) 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 https://github.com/zesterer/tao/issues/8#issuecomment-707232679 which can be added any time later to make the code type check without rewriting & refactoring huge portions of the code).

[VictorTaelin]

1. Yes, the syntax is actually much simpler on the current release. This repository is an archive, the language is now being developed here: https://github.com/uwu-tech/kind . Lots of new syntaxes, check SYNTAX.md. And it will get simpler every day

2. Everything MIT (see LICENSE on the repo above)

3. We're working in one now! Based on inets. But in our spare time. If you're interested in helping let us know!

4. Not sure I understand?

5. We kind have something like that for JS (importing and using a Kind library in JS is as easy as installing a normal JS module). But I'm not that proficient with C. So I'll accept inputs and opinions of these more experienced with the language.

6. The way we do errors is optionals (i.e., Maybe, Either), and monads really help making them much more manageable and joyful to use. Are you used to Haskell's do notation? Also check the <> and without syntaxes on Kind. Simple stuff but really handy. To further improve that we'd probably go in the direction of algebraic effects.

7. Not sure what you mean, but I think you're talking about holes? For example:

Bool.not(a: Bool): Bool
  case a {
    true: ?a
    false: ?b
  }

?a makes the code check and allow you to fill it later.

[VictorTaelin]

@MaisaMilena is it possible to move this issue to Kind?