The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

We don't know! else it would have implemented already...
Anyway, there are several ideas of different paths that should be followed to 
design this next generation…

We would like to use already proved theorems and not tackle the translation 
of these proofs in the logic in witch we will prove the next theorem. Going 
mechanically from one theory to an other is studied around Dedukti for 
example. 

There are of course a lot discussion about underlying theory and what set of 
axioms we want. But in any logic you choose, you never write manually terms 
in the logic you uses.
There is a compilation process from the user language to the kernel one. 
Users needs to write and read terms, kernels should be trustable and 
consequently tiny. A compilation is involved, hopefully it is sound but there 
is often no simulation lemma. Reduction makes appears ugly non wished values 
that you would have never write and you are sometime incapable to read. 
Mathieu Sozeau in Equations works a lot around this problem.

During this compilation, higher order unification is involved. Once again, 
people work hard on that but practically implemented algorithms are both 
naive AND ununderstandable. Moreover, the lambda calculus takes all the space 
and work about inductive definitions have just begun. In that perspective, I 
know Agda and Beluga are one step further.

We don't know how to do libraries in dependently typed programming languages. 
There is barely no way to say "suppose I have this abstract type and these 
definitions/properties over it" because reduction on open terms is essential 
and breaks any abstraction you try to put. I don't know, for example 
FSets/FMaps/Numbers libraries try to find a way without finding an ultimate 
answer.

Let's talk about a tactics language now, we start to see some emerging 
attempts to build understandable ones but the zoo is a real mess! It has been 
part of the work done in Ssreflect, CPDT gives a completely different proof 
style. HOL light gives a third answer. 

About tactics themselves, We would like that the computer do more and more of 
the proofs for us but decidable theories/procedure decision aren't there yet 
… It is the duty of plugin makers, Isabelle is much more advanced in the 
process of talking with already existing external tools.

What is computer-human interaction in order to prove stuff ? Who really know, 
it is even not really a question for the mathematical computer scientist.
It seems that it is an incremental process where version control system 
answers can be reused…

Clearly solving goal is a video games

Like in  tetris-frozen bubble-…-like, you play a move depending of the 
environment you've created from your precedent moves. 
If in Doom, your favorite weapons becomes the easiest one to draw, tactics 
should be the same. 

We are still as linear as math are on papers are whereas we deals with 
forest. Why cannot I do like modern games where the play is a complete mess 
where I do things in "I don't know myself what order, doing stupid stuff and 
forgetting about them" and then I can watch a cinematic of the party where 
everything is so well organized ...

Efficientcy in IDE has to be invented. 

I'll stop here my partial survey by underlying the fact that proof assistants 
has becomed too big to be only one research topic !
Coq made its way during 25 years in the bazar and is stressed by very good 
mathematician and hackers so it is mature enough to resist to some assault 
but as a research tool and not a productivity one its main goal remains to be 
an experimental platform in order to find this next generation and not to 
reach an ultimate state ...

Pierre B.

> Le 18 déc. 2012 à 22:23, Victor Porton 
> <porton AT narod.ru>
>  a écrit :
> 
>> I think that Coq is a VERY good proof assistant.
>> 
>> Nevertheless I dare to ask this question:
>> 
>> What will be the next generation of proof assistants? How and in which 
>> aspects they will surpass Coq?
>> 
>> -- 
>> Victor Porton - http://portonvictor.org