Yeah, to me that's the real question: Can the language of proof assistance be efficiently used for general purpose programming? As you say, right now it's too

Yeah, to me that's the real question: Can the language of proof assistance be efficiently used for general purpose programming? As you say, right now it's too hard for general use.