3 ms·
The "hole-driven" development style originated in dependently typed languages such as Agda and Idris, which I imagine Matthew's video was inspired by. So if you
by rntz 10y ago
The "hole-driven" development style originated in dependently typed languages such as Agda and Idris, which I imagine Matthew's video was inspired by. So if you want to experience it right now, go learn Agda and use agda-mode in emacs. (Probably something similar exists for Idris. I don't know whether Coq has a notion of "holes".)
- chriswarbo 10y agoidris-mode for Emacs does similar tricks ( https://github.com/idris-hackers/idris-mode https://github.com/idris-hackers/idris-mode ) and I've heard it's very nice. The Idris REPL itself can do hole-based programming too, which can then be dumped out to a file (:m to list holes, :p to prove a hole, :a to write proofs to disk) http://docs.idris-lang.org/en/latest/reference/repl.html http://docs.idris-lang.org/en/latest/reference/repl.html