The problem of Section 4.1 illustrates that in mathematical computations, especially those that involve symbolic aspects, a significant deductive component is needed to manage the assertions, preconditions and other logical aspects of the computation. We believe that a formal, deductive component, like Nuprl, is essential for assuring that combinations of mathematical tools will perform correctly in concert. Towards this end we have been coupling Weyl and Nuprl to address problems that arise in computations in commutative algebra [53,54].
For example, formal definitions can be given for the indefinite integral of a function, for the value of the definite Riemann integral
and the relationship between the indefinite integral and the value of the definite integral. These definitions frame the task of a numerical routine that evaluates the definite integral using the formula of QuadIntegral:Eq, viz.,
But this numerical routine is only valid when 
is bounded
away from 0, as a very simple and shallow inference shows.
Once the mathematical types are given formally, there will be cases in which static type checking will guarantee that the expressions being used are sensible. Given a predicate ``RiemannIntegrable'' that determines whether a function is Riemann integrable over an interval, one can define the type of Riemann integrable functions:
The task of determining whether or not a definite integral has a well
defined value can then be viewed as type checking in as much as it asks if
the function
belongs to the type of Riemann
integrable functions for 
and 
.