Even if it was infrequent (I'd be interested in data too!), what do you do when it does come up? It's very difficult to constrain yourself to decidable domains

Even if it was infrequent (I'd be interested in data too!), what do you do when it does come up? It's very difficult to constrain yourself to decidable domains when you want to write arbitrary programs and capture arbitrary program properties. You could let the proof goal go through without a proof but you'd have to replace it with a runtime check otherwise if the goal happened to be false all your static guarantees are out of the window (like doing a bad type cast in C++ for instance).