What types are to mathematical proofs as types à la Martin-Löf are to constructive proofs, and what's wrong with them? The question is motivated by this surprising sentence from Freek Wiedijk's The QED Manifesto Revisited.

I agree that the QED-like systems that exist today are not good enough
  to start developing a library as is described in the QED manifesto.

Surprising to me, that is, who had not heard of the QED project before. 
(Edited after A. Bauer's answer) OK, time I mopped up. 
I was 1st introduced to the Curry-Howard correspondence back in school days long, loooooong ago; I understood it as s/th along the lines of "Any computer program is a constructive proof that inhabitation of its input type entails inhabitation of its output type"; my very next question was, "OK then, if instead of any program we restrict ourselves to programs that model mathematical proofs in classical logic, what would be the proper type system(s) for them?". I guessed it had to be existential types, guarded subtypes (meaning types restricted by any formula; so that you would write e. g. "let x: {r : Real | !(r : Rational)}" if all you mean is to express that x is irrational), or such like stuff; then I let the matter rest and turned to more pressing ones, to wit, getting a degree.
If I had pressed it further at the time &, instead of the title question, asked "What types are to classical logic as simple types are to constructive logic?", maybe I'd have been answered "There are no such types: there is no need to extend or otherwise modify simple types for classical logic, since it is encompassed in constructive logic. Go get some understanding of type theory, and learn how to do with them. " 
If I had asked again at the time the QED manifesto was issued, a plausible answer might have turned to "They're called refinement types. What's wrong with them is, they're a pointless gadget: the problem they solved was not a foundational one, and introducing them did not present type theory with any new challenge. So all the papers they deserve have been written already. "
Returning to it now, it seems to me the natural way to attack the QED challenge would be: 1. to set forth a serious answer to my old question, 2. design the corresponding language, 3. build the proper language tools, including, in the end, a full-fledged proof assistant (probably posing as a type checker), 4. look what happens. In a programming language with refinement types, the C-H correspondence now works as: subprograms returning (refinements of) void model conjectures, their bodies model proof outlines, assertions in the bodies model steps in the proof, Skolem functions arise naturally if handlers for failed assertions are allowed. Then, verified theorems in predicate logic are those subprograms in which the type checker has been able to reduce all assertions  to tautologies. 
What hopefully would happen if a suitable extension to such a language had become popular is, useful tools could start developing, such as doclets to turn fragments of source code to academic papers; people might get used to writing in it just to convert formulas from .pdf to .ps, or to save themselves the hassle of adjusting to the style guides of every other journal they submit to; later, we might dream of replacing arXiv with a global GitHub repository of their works. This could take place long before any proof assistant worth mentioning existed for the language. 
Given Wiedijk's paper though, the real story must have been quite different. It reads like people trying to endow dependent types with refinement soon hit some snag and, instead of developing proof assistants (Edit: read formal languages and tools) for classical logic, they went happily to rewrite classical math for constructive logic. 
(Edit) With predictable results: mathematicians have been accepting a certain style of proof outline for some time now and non-mathematicians are used to it, so if it is too arcane work to make it understandable by a automated checker, they will rather dispose of the proof checker than of the proof. 
Turn away for a minute from what dependent types mean, and look how they would be used in a language purporting to be strongly typed. The user is student X with a major in control systems, a hobby in Java programming, currently at grips with an intro to topological groups. So far, he has managed to translate "pick any dyadic integer " as "let x: Integer(2)"  for proof-checking freeware he downloaded a minute ago, then "consider first the case of a rational integer" to "let x1:Integer(2)*Rational"; now attacking "pick some irrational number x and consider the fractional parts of the p.x's, p ranging over Z: obviously, blah blah blah". Not understanding a word of type theory, he first looks for a way to say "let x: Real - Rational",  finds none, looks harder, still finds none, then let go & turns back to more pressing matters, to wit, control systems. 
Of course, if student X had access to such a language as I sketched, he would have given up long before he got any proof automated. No harm done, though: what he wants is to understand TG's, not that a computer program understand it in his stead, nor to understand type theory. All he needs is to keep his fingers busy while reading, and I advocate giving him a productive way to do just that.  
My read of Wiedijk's paper is, if you bar student X from modelling things the way he understands them, he will turn to  what he considers more pressing matters, regardless of how pressing your need for computer-checkable proofs, and how deep your understanding of what the modelling language guarantees. It explains how we still lack a free-access, widely-known, low-quality, multi-audience, computer-interpreted codebase of mathematical theories the way we have a free-access, widely-known, low-quality, multi-audience, human-readable textbase of common lore. 
Edit Just to clarify: the codebase of mathematical theories in question would still be as far away from being computer-checked, as is WP from auto-generating ontologies for the subject matter of its articles; light-yrs away. The (hopeful) progress lies in the rest of the road being mostly for metamathematicians & software engineers to tread, with the part of "ordinary" mathematicians perceived as non-problematic. 
Hence my question: what type systems are the natural ones to express assertions in classical logic? Or maybe I should have titled this post "What types are to dependent types, as refinement types à la Freeman-Pfenning are to simple types?". Anyway, what have they that makes their theory so unsavory? 
 A: A good starting point to learn about type theories for classical logic is the $\lambda\mu$-calculus introduced in 1992 by Parigot in λμ-Calculus: An algorithmic interpretation of classical natural deduction, which extend the $\lambda$-calculus to give a computational interpretation of classical natural deduction.
For the next step, I would recommend reading the research summary on Hugo Herbelin's home page. Chasing some of the references listed there, you will learn how incorporating control operators into type theory yields a computational understanding of excluded middle.
For a modern take on the role of excluded middle in Martin-Löf type theory I recommend reading at least Section 3.4 of the HoTT book. The important bit to take away from there is the fact that excluded middle can coexist with the rest of homotopy type theory quite naturally.
You speak of proving correctness of programs, possibly using classical logic. For that you can use a system based on refinement types, such as F*. Also note that proving correctness of programs is an activity unlike formalization of traditional mathematics, so do not expect a single tool to work equally well for both of them.
In my opinion the presence or lack of excluded middle in a proof assistant has very little to do with it being useful for formalization. Of course, if you want to formalize classical mathematics then you need excluded middle (but much less frequently than most mathematicians expect). Most modern proof assistants let you postulate excluded middle quite directly and use it to your heart's content, so that cannot be the show stopper. One of the most popular proof assistants is Isabelle/HOL, which has excluded middle built in, but that does not make it significantly more successful in comparison with other formalization tools.
It is a bit difficult to understand what precisely you are getting at in your long discussion, but I would venture to say that you've misidentified negation and excluded middle as the culprit. I am not even sure whether you think that Martin-Löf type theory has no notion of negation – of course it does! In fact, the problems faced by your student X has nothing whatsoever to do with type theory. Student X would face essentially the same obstacles if they used any other formal system, such as first-order logic and set theory, or higher-order classical logic. Your student X is quite naive to think that formalization of mathematics is just a simple exercise in translation from English prose. It may be true that usability is decided by the users, but the users' abilities play a role as well.
