lean3

Sort of the official policy is that inside proofs (i.e., terms of types in Prop) constructibility doesn't matter, but inside definitions (i.e., terms of types in Type 0 and above) try to be constructive. For example, it is ok to define a function constructively but with a nonconstructive proof of termination. LEM is used everywhere because it's actually a theorem. It follows from functional extentionality and the existence of quotient types. https://github.com/leanprover/lean/blob/master/library/init/... The axiom of choice is an actual axiom, and it too ends up being used everywhere, but mostly to introduce decidable instances to permit things like double negation elimination inside proofs. An illustration: [1] introduces these instances to the file and [2] implicitly uses the instance. [1] https://github.com/leanprover-community/math

Plus, it's a theorem in Lean: https://github.com/leanprover/lean/blob/master/library/init/... (Lean has a somewhat different type theory from Coq, where propositions in Prop have the property that all proofs of a property are defined to be equal. It turns out this along with functional extensionality (that two functions are equal iff their evaluations are all equal) is enough to get LEM, but only in Prop. Outside Prop there's a stronger commitment to constructibility. Still, every definition and lemma has some program backing it.)

I'm not sure what you're talking about, unless you're saying truth is provability. (Classical logic would disagree.) The Lean proof assistant, which has a pretty strong commitment to constructability, has the law of the excluded middle just fine: https://github.com/leanprover/lean/blob/master/library/init/... The caveat is that it only exists in Prop, and it's a consequence of proof irrelevance and functional extensionality. Types outside Prop don't have it for the simple reason that there's no sensible way to construct an element of Either A (A -> Void) in general (this is quasi-Haskell notation, where Void is a type with no terms). I'm not sure there's any need to bring Godel into this....

For people interested in using Lean, note that there's a community fork (https://github.com/leanprover-community/lean) of the last official Lean 3 release 3.4.2 (https://github.com/leanprover/lean). The fork is still under active maintenance, so might be a better place to start (the main development team have moved onto developing Lean 4.0 (https://github.com/leanprover/lean4), and it's not clear when that will be ready).

Lean. It's implemented in a dependently typed programming Lean is implemented in C++ [1, 2]. There's a message in there somewhere. The message is probably something along the lines of: if you want performance, use a low-level language. [1] https://github.com/leanprover/lean/tree/master/src [2] https://github.com/leanprover/lean4/tree/master/src