Why does it rely on the axiom of choice? It’s a consequence of the obvious fact that for every integer n, there exists a program that prints n. This doesn’t require choice.
(I agree that there are formulations which don't require LEM, but it's important to be precise, especially when writing to dismiss a common misconception among people who haven't got the concepts crisply in their minds. "Is this quantity computable?" is very close in spirit to "can I compute the value of this quantity?", and LEM is exactly the kind of axiom which shows the difference.)
> Ex-falso has trivial computational content, and we use it all the time: it's `panic!()`.
I have major issues with the computational content of a bottom type; my interpretation of the BHK semantics would not admit ex falso as constructive.
Of course this all of this really stems from one’s notion of semantic truth: any non-trivial semantic theory of truth can be argued as the “one true logic”, and there’s not much anyone can say otherwise! As I see it, it really comes down to how useful it turns out to be in modelling the particular domain of discourse.
As it happens, I’m more than happy to accept classical logic: I believe the principle of bivalence is how the world works, and as a result I’m forced to admit LEM if I want my proof calculus to be complete.
You are right that pointing out the connection to LEM is important and worthwhile, regardless of formulation.
If you’re going to quibble over whether LEM is justifiable in this case, then you need to justify why you’re only concerned about LEM; why not drop ex falso too (Kolmogorov had serious issues with this axiom, and initially considered it to be incompatible with a constructive logic) and work in a paraconsistent logic?
Also, depending on the precise formulation of this proposition, it doesn’t necessarily need LEM.