|
|
|
|
|
|
by Syzygies
2 days ago
|
|
|
https://github.com/Syzygies/Compare I spent far too long comparing dozens of languages, only some of which are part of the above project, before switching from Haskell to Lean for a new phase of my math research. Lean wins for me without considering or using dependent types (for now). It is simply a better programming language than any I have seen. This is a critical advantage for those interested in proof. One codes tactics using the same language as for proof. https://github.com/Syzygies/Compare/blob/main/source/lean/Na... I do have a future interest in proof, giving Lean an edge for me. I prefer my symbolic reasoning in visual form. I anticipate a future where we draw and view AI drawings, and see any printing press derived notation as antiquated as cuneiform. The above image is a possible language for representing the first Lean proof in "The Natural Number Game". About one in ten mathematicians that I show this to can grasp it much faster than the Lean notation. The other nine imagine a visual programming language to be something like a PowerPoint slide or a children's graphics language, and don't see the point. |
|
|
