The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

I am very happy to read about Kinan's example!  I am a software
engineer with very little prior exposure to proof systems, yet I was
able to pick up Ltac rather easily and be somewhat successful with Coq
despite not knowing much about Coq's underlying theory.  It is
comforting to know this is a more common experience.

I'd like to amend my previous comments.  This is not the first time
I've had some fears about proof systems like Coq leaving software
engineers behind for the loftier ambitions of mathematicians.  I also
felt that when the HoTT people first gathered here years ago.  I'm
very thankful when mathematicians make contributions to proof systems,
but worry that they will use their abilities and influence to tune these
sytems more to their own liking and less to mine, and others like me.

So I think most of my own reaction is to the tone of some of the
pro-Lean comments in this thread - they sound to me as though they are
suggesting that their way is better and Coq would be foolish not to
follow their lead.  "Lean is like Coq but better" ... perhaps for some,
but not all.

On Thu, 9 Jan 2020 04:33:01 -0500
Kinan Dak Albab 
<babman AT bu.edu>
 wrote:

> This has been an interesting discussion to read. I do not have nearly
> enough depth in fields medal level mathematics or the career and
> politics of being a mathematician to understand all the subtle
> implications of having a purely constructive vs classical reasoning
> framework on that world. However, I want to add something to a
> previous point, although the discussion seems to have drifted away
> from it.
> 
> I think Ltac deserves more credit than this discussion was giving it.
> I taught a course last year where we covered using several proof
> assistants and certified programming languages (from the program
> verification perspective) to students of various backgrounds, from
> undergraduate seniors to PhD students. After about 4 weeks of Coq,
> most students were able to write small but non-trivial tactics for
> program verification, either to shorten their proofs by repeating
> some proof pattern directed by the structure of the program being
> analyzed (e.g. applying case analysis on the condition in an if
> statement), or for crunching/generating sub-goals with Hoare logic
> etc.
> 
> Most of these students did not have prior background on this kind of
> formal reasoning or proof engineering, but they were able to use and
> intuitively understand props and inductive relations in Coq because
> of their computational content / interpretation. It was considerably
> more challenging for the students to do something similar in Lean.
> The theorems and programs they were able to work on were considerably
> simpler. Part of this may be because I am far more comfortable with
> Coq, so I may have given better examples or homework exercises. But
> it was clear that (at least for program verification) tactics are
> really as important as library theorems and lemmas (if not more so).
> 
> I am not entirely sure that providing extensions of any specific
> system that incorporates different axioms (e.g. LEM) is the way to
> go. I agree with Talia that having different systems that cater to
> different communities is perfectly fine, provided that interfacing
> between such systems is improved. The main shortcoming of the status
> quo (from my very pragmatic program verification perspective) is the
> immaturity of programming/proof abstractions for proof engineering,
> which fail to sufficiently abstract the mathematical foundations of
> the system, and end up increasing the learning curve and required
> background for effective use of the system. It is ridiculous to
> assume that programmers who use strongly typed programming languages
> need to understand the underlying type theory and logical foundations
> well, in fact most do not. Unfortunately, this seems to be a
> requirement for those interested in mechanized proof engineering.
> Customization is likely to make this worse.
> 
> -Kinan
> http://cs-people.bu.edu/babman/
>