Their goal is also to rewrite all of mathematics in a constructive way,
This is not the goal of HoTT, and also not possible as some mathematics is intrinsically non-constructive.
HoTT allows non-constructive reasoning, see section 3.4 "Classical vs. intuitionistic logic" of the HoTT book http://homotopytypetheory.org/book/. You can say that HoTT derives non-constructive mathematics on top of constructive foundations.
The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive)
No. Whether a proof can be logically checked by a computer has nothing to do with whether it is constructive or not. A proof is just a syntactic object. It's just as easy to check if a proof step uses excluded middle or double negation as it is to check whether it uses a construtive principle like /\-introduction. There are many proof assitants that work with classical logic, e.g. Mizar, HOL, HOL light, Isabelle/HOL ... All of SAT-solving works classically.
The novelty of HoTT, and only extension over intensional Martin-Loef type-theory, is the univalence axiom.
A proof in mathematics is not purely syntactic because it's not purely logical. For instance, in some steps of a proof, we do something to both sides of an equation and argue that it is still balanced, based on rules that are outside of logic. Such a step can have a nonconstructive element.
A proof in mathematics is not purely syntactic because it's not purely logical.
This is confusing constructive reasoning with the decision problem for proof validity. They are different things.
The very point of logic, constructive or otherwise, or at least one of the key points for having a logic is to be able to decide whether a given proof object is indeed a valid proof. Valid proofs of course typically also make use of non-logical axioms of the ambient theory. If proof-hood is not decidable, it's not a logic.
Reasoning is constructive if it avoids certain proof principle like LEM (law of excluded middle) or double negation.
Classically, LEM and double negation are equivalent.
Intuitionistically the situation is more complicated, see the discussion in this thread by IngoBlechschmid: We can prove that LEM implies double negation, but not the other way around. Intuitionistically, we can only prove that ⊢¬¬A⊃A, then ⊢A∨¬A, but not ⊢(¬¬A⊃A)⊃(A∨¬A).
For these and related reasons, double negation is not considered constructivistically valid.
HoTT allows non-constructive reasoning, see section 3.4 "Classical vs. intuitionistic logic" of the HoTT book http://homotopytypetheory.org/book/. You can say that HoTT derives non-constructive mathematics on top of constructive foundations.
No. Whether a proof can be logically checked by a computer has nothing to do with whether it is constructive or not. A proof is just a syntactic object. It's just as easy to check if a proof step uses excluded middle or double negation as it is to check whether it uses a construtive principle like /\-introduction. There are many proof assitants that work with classical logic, e.g. Mizar, HOL, HOL light, Isabelle/HOL ... All of SAT-solving works classically.The novelty of HoTT, and only extension over intensional Martin-Loef type-theory, is the univalence axiom.