[FOM] Formal verification

[Dominic Mulligan]

>  I would be interested to know what, in the view of those who know about
> the current state of things, is the main current obstacle to a wider use of
> computer verification in the medium term (say the next 10 years):
>
>
>
> a) Competing systems and paradigms in the formal proof community;
>
> b) Lack of engagement from ‘mainstream’ research mathematicians;
>
> c) Lack of funding;
>
> d) Some fundamental issues on a theoretical level that still need to be
> overcome?
>
>
>
A lack of libraries is a major issue. It's hard to start formalising
research level mathematics when large swathes of undergraduate mathematics
is still missing from the libraries of the main proof assistants. Further,
what exists is coloured by the biases of those who use the systems, mainly
computer scientists: there are a lot of formalisations of things like red
black trees and typed lambda calculi, for instance, whereas continuous
mathematics seems to be neglected, or at least it seems to me.

Further, libraries implemented in a system based on type theory like Coq or
Agda are useless if you use Isabelle or HOL4, systems based on HOL. Even
the statements of theorems and techniques used to formalise e.g. matrices
and linear algebra would need considerable work to port from Coq or Agda to
Isabelle due to the vastly different foundations of the two groups of
systems.

>  PS. Some years ago I actually tried to contact people in the Mizar
> community to try and find out what it would take to verify some of my own
> results with more elementary proofs. However, I never received a response,
> and found the documentation available rather impenetrable. I was also put
> off by the impression that it was not possible to run Mizar
> “conditionally”, i.e. formalize the statements of some standard results and
> verify a proof subject to their correctness – which is inevitably going to
> be necessary in the initial stages if verification is to be brought into
> wider mathematics.
>
I think this is possible in all modern systems. You should consider looking
at Isabelle or Coq if you are still interested in pursuing this.

Regards,
Dominic Mulligan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20141020/d3c3c0e1/attachment.html>