ABSTRACT
Many applications in image processing, control
systems and other areas, have very well understood
mathematical models. Optimization problems, in particular,
are a class of (implicit) models which is particularly
useful. When faced with the task to develop such an
application, a software engineer aware of best practices
might use a computer algebra system to compute some
problem-specific quantities which are then put into a
simulation environment (such as Matlab), and ultimately
translated to code. Such a process requires the development
of multiple versions of the mathematical model, often by
hand, in tools with widely varying levels of formalism,
which are generally susceptible to soundness problems.
Moreover, it may be very difficult to decide whether the
various models are in fact equivalent. Through an extended
example of a multidimensional Newton’s Method, we
demonstrate how computer algebra and theorem proving
systems can be used to largely automate this process. We
compute problem-specific quantities, including higher-order
ones, verify their correctness, and automatically generate
code which is verifiably correct. The process combines
untrusted components with trusted ones so that failure in
an untrusted component is always detected.