Implementing an "autocheck" for various types of computation makes
good sense, within a software testing environment. Using it inside the
actual computations is generally a RBA ("real bad idea"). There are
exceptions, e.g. using numeric checks to discard parasite roots in
algebraic system solutions. But that tends to be a fairly well defined
area.

It is an open question of whether and when to use such checks
automatically in symbolic integration. Unlike algebraic solvers, there
are myriad problems lurking. I'll name a few.

(1) The symbolic integral might contain functions that are slow to
numerically evaluate accurately.

(2) The checks involve quadrature. This can be significantly slower
than the symbolic integration, particularly as dimension increases.

(3) Quadrature can be prone to errors.

(4) These only are applicable when no parameters are present, or
numerical values within assumption and proviso ranges (if any) have
been selected for the parameters.

None of these impede the use of such checks in the QA process. They
simply mean that such a check is difficult to make within the symbolic
integration itself.

(1) I've seen ample reference to a document claiming another program,
Maple, has "dozens thousands distinct bugs" in some version, possibly
aple 9.5. Said document is partly correct in that it shows clear sign
of the "dozens" distinct bugs. But the "thousands" part was suspect
(okay, conspicuously absent), and really was ly repetition of the same
underlying defects as were categorized in the "dozens".

Point being, from past history I'd be inclined to believe the part
above about MuPad having "many" distinct defects. But I'd not take
seriously the "thousands" claim without independent corroboration.

(2) The claim originally was that exact integration is not likely to
use a numeric check. This reluctance can contribute to some level of
bugginess but I rather doubt it contributes to much, given the
impediments to implementing it well.

(3) It may well be the case that SciFace GmbH uses such methods in
their QA testing processes. The original remark, again, was simply
that it is not readily used in symbolic computations themselves.

Case in point: Integrate in Mathematica does not at this time use
quadrature checks via NIntegrate. But they are used, and in some
places automated, in the testing of Integrate. My opinion is if we
tried to add such quadrature checks to Integrate itself, we'd break
more than we fixed.

(4) Those who write, maintain, and (at least for the commercial ones)
market computational math programs need to have a sense of where to
place finite resources. It is quite possible that the MuPad developers
simply disagree with your implied claim that symbolic calculus is a
high priority area.