I think Edwin Brady also does.

Idris code is short and clear.

There is much less of it – for instance, as a kind overly specific example, serializers/deserializers and API code can be automatically generated from the model definition.

Idris code tends to sort of “fold in” test code into the function definitions themselves, so you do less work AND it’s much more rigorous.

Then there’s the compiler IDE interface which is explicitly intended to be an upstanding citizen in developer workflows.

I also want to mention how easy it is to write Idris compiler backends for any given language. This is on purpose, and is made possible by what Idris is: It’s dependent types, and dependent types is automation of the automation.

So it’s not a question of “making muggle developers eat their formal vegetables” or the like. It’s that when the automation of the automation hits, it makes work so much faster and more efficient and more pleasant that it outcompetes the slop because slop is slop. Idris might be that automation; It might not. We’ll see, right?

I’ve picked this hill to die on. At least one death, of something. Maybe just a feeling or a hope, but something.