The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Quotient reasoning isn’t used enough in program verification because we are 
used to think in terms of syntax missing many tricks which are based on a 
more semantic perspective and which lead to nicer structures. An example is 
the treatment of non-termination which is often addressed by some fuel based 
approach. We have shown that non-termination is a monad given by the free 
omega-cpo over a given set (in the sense of HoTT) using a quotient inductive 
type. More needs to be done but there is the potential to actually use the 
ideas from domain theory in practical program verification.

Sent from my iPhone

> On 3 Jan 2020, at 13:34, Adam Chlipala 
> <adamc AT csail.mit.edu>
>  wrote:
> 
> On 1/3/20 7:37 AM, Thorsten Altenkirch wrote:
>> Both Coq and Lean fail in properly supporting structures with a 
>> non-trivial equality. Lean doesn’t really offer an answer to setoid hell 
>> but just adds quotients as an axiomatic principle with no computational 
>> explanation. This is despite us knowing since a while (I wrote a paper on 
>> this in ’99) how to turn setoid hell into setoid heaven by working within 
>> the setoid model: that is if you want to talk about setoids all the time 
>> just accept that every type comes with its own eqaulity and build your 
>> type theory around this.
> I think one factor that might lead to surprisingly different perspectives 
> from different people in this discussion is that, as far as I can tell, 
> quotient reasoning is much more common in pure math than in program 
> verification.  Yes, it comes up often enough that everyone working on 
> program verification has used it in a few projects, but it hardly seems to 
> rise to the level of an essential foundation for all work (which raises 
> questions of whether it is worth complicating the core type theory to 
> support, expanding the trusted base).  I don't think too many 
> program-verification projects are avoiding quotient reasoning because it is 
> awkward rather than just not especially applicable.



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.