I know very little about what I am talking about in what follows, so I appreciate any all help in pointing out all of my mistakes -- otherwise I won't be able to learn more and advance in my knowledge of these interesting subjects.
I want to learn about lambda calculus because it seems like an interesting way to think about functions in general, and because a generalization called the stochastic $\pi$ calculus studied by Luca Cardelli and others seems to allow many computational interpretations of biology, something which I am really interested in. Also other reasons, like wanting to learn and understand functional programming, in order to have an alternative to C++ which I dislike.
However, I just learned that type theory, at least as stated by Lof, is supposed to be a way to formalize intuitionistic logic/constructive mathematics, which rejects the Law of the Excluded Middle and even the Axiom of Choice. My background is more in mathematics than computer science, so although I can see how having to construct something to prove that exists is an acceptable restriction for people interested primarily in computation, I am really uncomfortable with having to give up proof by contradiction and the Law of the Excluded Middle. Perhaps that makes me old-fashioned, and my grandkids will laugh at me for this concern, but proof by contradiction can be very useful and is how I learned a lot of the math which I know.
Is there a way to learn about $\lambda-$calculus and type theory while at least being agnostic about the Law of the Excluded Middle and not outright rejecting it?
The discussion on p.9 of the Homotopy Type Theory book seems to say something to the effect that Univalent Foundations and Homotopy Type Theory can be compatible with the Law of the Excluded Middle and the Axiom of Choice, even though they contradict the univalent axiom? Needless to say I did not quite understand the argument about (-1) types and thus am still somewhat skeptical and unconvinced.
Also, in one of his lectures at the Oregon Programming Language Summer School posted on youtube, Professor Awodey, one of the big names behind the IAS's Homotopy Type Theory/Univalent Foundations Project, seems to identify the Heyting algebra as underlying logic, rather than the Boolean algebra. I read somewhere else (I forgot where unfortunately), that Heyting algebra is what results if one rejects the Law of the Excluded Middle, and thus presumably founding logic upon Boolean algebra means accepting the Law of the Excluded Middle.
Ideally I would prefer to not have to choose between $\lambda$-calculus and Boolean algebra, since the latter underlies most of my understanding of logic, and is also the basis for probability theory, which I know very well and would not like to give up or reject as half-baked. Also I thought Boolean functions were a very hot topic of computer science research, so it seems kind of strange that some computer scientists would prefer Heyting algebra.
These questions might be relevant: Where is the proof that Coq + Excluded Middle is consistent
Heyting algebra in simply typed lambda calculus
Can boolean algebra be expressed in simply typed lambda caclulus?
If they even answer my question, would you mind explaining to me how (as if I were five, so to speak)? I don't quite understand the discussions on them.