Very nice descriptions. While constructive reasoning is has many advantages, it has one disadvantage that is rarely pointed out, but sometimes causes real trou

Very nice descriptions. While constructive reasoning is has many advantages, it has one disadvantage that is rarely pointed out, but sometimes causes real trouble. Let's say we have a formula A which is classically and constructively true. It may be the case that constructive proofs of A are longer and more complicated than classical proofs of A. If you are working with an interactive proof assistant, this may be the difference between the proof automation being able to deal with A automatically or not. This explosion in proof size is the reason why the (perfectly constructive) nominal techniques of Pitts et al have been implemented to a high standard in Isabelle/HOL are are used frequently, but are not really in Coq.