I've been thinking that maybe the future of human computer interaction in general is all through the front door of an LLM utilizing a suite of well known formally verified tools which compose (think UNIX pipes, redirection) with the ability to write and formally verify tools on the fly. We're pretty far off in terms of compute ability but I suspect our grandchildren will look at us human code writers as we look at the sliderule wielders of yesteryear...