Agda literally has this "hole-driven development" as a standard feature in its IDE modes. Not only that, but when developing Agda code you get a list of every binding in scope, as well as a prompt of the type that must be provided to resolve the "hole". The expectation is that every part of developing Agda code can be expressed as a kind of "autocomplete", if desired.