Holes in Agda are a good bit more powerful than in Haskell, and agda's emacs mode has a bunch of very powerful commands for working with them, eg: listing possible values, automatically filling, splitting them by case, etc.

For example, for this post's "jonk" example I just had to copy the type into emacs, reformat it a bit into Agda syntax, then press C-c C-a and it automatically figured out the solution that the author worked through manually: λ z z₁ z₂ → z₁ (λ z₃ → z₂ (z z₃))

See the full list of commands at https://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html

Check out Idris and the book Type Driven Development. It has an emacs mode that does that for you. I’m not sure about other languages. It was a very nice experience though I just went through it for the learning experience and haven’t tried to apply it to any problems since then.

Why even have the code? The type is all the compiler needs to spit out a definition. Your source can just be the type.

Idris does this with a REPL-like interface:

https://www.youtube.com/watch?v=mOtKD7ml0NU

Intellij can sorta do this for Java if you fo ctrl+shift+space.