The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

Careful, a small TCB is very much a Lean-ism 😜

Sent from my iPhone

> On Jan 3, 2020, at 6:35 AM, 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.