> I'm not very happy with the computational content of LEM > Ex-falso has trivial computational content, and we use it all the time: it's `panic!()`. I have m

> I'm not very happy with the computational content of LEM > 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.