Kind2 VS hebigo

Agreed. Even from a PLT perspective, I prefer Kind2 by the Kindelia Foundation for supporting inductive theorem proving (and hopefully some level of dependent types), as well as being faster to boot.

I agree. Keep in mind our language (Kind-Lang) does target the HVM, and it is really promising. The type-checker is the fastest among proof assistants, by far; the error messages are really nice; it has a fully dependent type system which is a breath of fresh air to work with. It is still not production ready though (mostly due to lack of IO), but is the extend of our effort on that direction. We hope other lang developers get encouraged to target the HVM to. Elm and Idris are great candidates for that IMO.

Another very small proof system: https://github.com/moonad/formcorejs

The core implementation is under 700 lines of JS, including the parser: https://github.com/moonad/FormCoreJS/blob/master/FormCore.js

The author has since moved on to building a runtime with optimal evaluation (https://github.com/kindelia/hvm) and a new proof language on top of that (https://github.com/Kindelia/Kind2) with considerably better performance than existing proof systems.

The Lissp transpiler incrementally compiles and executes each top-level form to Python. It needs to do this in case there's a macro definition that might affect the compilation of a subsequent form. If it's only executing definitions, this is harmless, but if you want to precompile the main module, it needs the guard, or the side effects will happen too.

If you want Python to be as customizable as Lissp, check out Hissp (and Hebigo).

Python's lambdas can have as many lines as you want. Just wrap parens around it. Hissp uses this form as a compilation target. Its REPL shows the Python compilation. Play around with it til you get it: https://github.com/gilch/hissp

The original Lisp's S-expression syntax was just supposed to be an intermediate language used by the compiler when processing the real language based on M-expressions, which kind of never took off. Numerous alternatives to S-expressions have been proposed, and some retain homoiconicity, another feature diagnostic of a Lisp (and one that ECMAScript lacks). For example, see Hebigo's readme, which shows a direct correspondence between its Python-like syntax and that of Hissp's default reader (Lissp), which uses the S-expressions. Julia can also be written in S-expressions, but this usually only used in macro definitions.

I think LoL is too CL-specific. If you know both languages first, you can pretty much translate, but since they'd be trying to learn Lisp in the first place, this is a bad idea.

On the other hand, [Hissp][1] has a pretty good tutorial for anyone coming from a Python background.

[1]: https://github.com/gilch/hissp

Hebigo: a whitespaceLisp isomorphic to Hissp that looks like Python.