Post #2798894

@ejgallego blew my mind with a demo where he had an imperative language embedded in Lean (always nice, of course, but nothing new so far), and then vibe-coded a debugger for it, with a graphical UI and DAP support, on top of it. This really makes #Leanprover shine. More details at https://www.joachim-breitner.de/blog/819-Vibe-coding_a_debugger_for_a_DSL