3 ms·

I personally prefer Agda to Lean or Coq [1] to prove my theorems but this frontier is imho among the most exciting research in theoretical CS in many many decad

I personally prefer Agda to Lean or Coq [1] to prove my theorems but this frontier is imho among the most exciting research in theoretical CS in many many decades. I really wish more programmers and mathematicians knew about automated theorem proving and automated reasoning. It's nothing short of revolutionary and I think next generation of pure mathematicians will use these as a crucial tool in their research. [1] It's a personal preference but Agda is simply a much better language with almost limitless metaprogramming which allows me to write proofs close to as they'd appear in prose math papers. It has a smaller ecosystem though. I've never seen a proof in any other language I personally didn't think would be much more readable/simpler in Agda.

IngoBlechschmid 1y ago
I'm currently creating an interactive tutorial on Agda, with lots of embedded exercises (running purely in the browser/on a server, no installation required), perhaps it is useful to some: https://lets-play-agda.quasicoherent.io/ https://lets-play-agda.quasicoherent.io/
gopiandcode 1y ago
Oh, really? I'm curious what exactly you mean by limitless metaprogramming. I've really been drawn into Lean specifically because of how easy to extend and malleable the language itself is, so if Agda is even more so then I'd be really eager to try that out. e.g.: - embedding a prolog/asp DSL: https://github.com/kiranandcode/cleango https://github.com/kiranandcode/cleango - embedding a tex/latex DSL: https://github.com/kiranandcode/LeanTeX https://github.com/kiranandcode/LeanTeX
- yuppiemephisto 1y ago
  I was surprised to hear their claim about Agda's metaprogramming, I say lean is better here
m_j_g 1y ago
Did you played with cubical flavor of Agda? here is fun project of mine related to it : https://github.com/marcinjangrzybowski/cubeViz2 https://github.com/marcinjangrzybowski/cubeViz2 :)

IngoBlechschmid 1y ago

I'm currently creating an interactive tutorial on Agda, with lots of embedded exercises (running purely in the browser/on a server, no installation required), perhaps it is useful to some: https://lets-play-agda.quasicoherent.io/ https://lets-play-agda.quasicoherent.io/

gopiandcode 1y ago

Oh, really? I'm curious what exactly you mean by limitless metaprogramming. I've really been drawn into Lean specifically because of how easy to extend and malleable the language itself is, so if Agda is even more so then I'd be really eager to try that out. e.g.: - embedding a prolog/asp DSL: https://github.com/kiranandcode/cleango https://github.com/kiranandcode/cleango - embedding a tex/latex DSL: https://github.com/kiranandcode/LeanTeX https://github.com/kiranandcode/LeanTeX

yuppiemephisto 1y ago
I was surprised to hear their claim about Agda's metaprogramming, I say lean is better here

m_j_g 1y ago

Did you played with cubical flavor of Agda? here is fun project of mine related to it : https://github.com/marcinjangrzybowski/cubeViz2 https://github.com/marcinjangrzybowski/cubeViz2 :)