Re:Talks that changed the way I think about programming
by rntz on Thursday December 08, 2016 @07:14AM
(#13129855)
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".)
[ Parent
| on HN ]
Re:Talks that changed the way I think about programming
by chriswarbo on Thursday December 08, 2016 @07:37AM
(#13129910)
idris-mode for Emacs does similar tricks ( 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