In Kevin's example where you have two programs, one which depends on the Riemann hypothesis being true and the other which depends on it being false, is that you can't just execute the programs -- they might have undefined behavior since they depend on the truth of some statement during their executions, and there's no general algorithm to decide whether undefined behavior is happening. They depend on undecided facts, so you can't put them together into a single program that decides the result. (Maybe a slogan is "truth can be contingent, but data cannot be.")

In Lean syntax, this is an example type signature of something that takes two programs (h and h') that respectively take in the truth/proof of a proposition or its negation, along with a proof that there is at most one element of α, and produces that element. I don't think there's a way to write this definition in Lean without marking the definition noncomputable:

  def extract {p : Prop} {α : Type*}
    (h : p → α) (h' : ¬p → α)
    (unique : ∀ (x y : α), x = y) : α := sorry

That’s where opinions will differ. That’s only true if you accept the law of the excluded middle.

Mainstream math does, but most constructive math does not.

Yes, Kripke semantics makes sense of constructive logic. Topos theory, too. But I really think of all of these embedded in classical logic, and assuming that the law of excluded middle doesn't hold for general reasoning just doesn't make any kind of sense to me.