Holes in your program (re: Azorius vs Simic at the compiler)

So I was reading idiomdrottning's post

Azorius vs Simic at the compiler

and I wanted to make a slight defense of dependent types *as* exploratory, iterative programming.

The language in the little typer isn't the best example of this. The language itself is really minimal and doesn't end up having all the bells and whistles of a real dependently typed system *but* as someone who worked on these sorts of things a lot as a grad student I wanted to talk about what using an Agda or an Idris feels more like.

It's like a conversation with the computer, a group project. You write your first attempt at types and then use those to generate the structure of your type directed functions, and I do mean generate. A lot of dependently typed programming languages that have text editor integration will fill in the skeleton of what the program must be by the induction principle of the type, giving you a bunch of "holes" to fill in for your code. You can fill in those holes piecemeal and even be working on defining your theorems and properties about your code simultaneously.

Even filling in the holes is done interactively as you can try out expressions and type check them before committing to them as filling in the hole or you can do case analysis on variables and have the type information revealed flow backwards into the rest of your code. For example, if you have a proof that the particular case is impossible then you don't have to fill in the hole, the typechecker understands the case is unnecessary.

It's kinda hard to explain this verbally but as I'm writing I am far too tired to install Agda on this re-OS-ed laptop and put together a real example. Maybe I'll do that in the future to explain what I mean.

I can describe the experiential part, though, which is that to me it actually does feel like

> I’m more of a hack hack, explore, evolve, iterative incremental improvement, big ball of mud, foot gun, intuitive programmer. Leaning into emotions and heuristics and hammock time and smells and refactoring.

but for math dweebs---such as myself, obviously---but it's still exploratory the same way live coding music and art is.

It's a process that I find very symbiotic, really, and less antagonistic than the typical "write code => does it work => aww fuck" loop.