Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?

[Nicolas Alexander Schmidt <zero@fromzerotoinfinity.xyz>]

Dear Bas, Michael, David, Valery, Martín and Kevin,


thank you all for your replies. When I posed my question, I didn't
expect there to be so much room for debate. In particular, I am
surprised that it seems not at all clear how much univalence actually
helps the practicality of doing formal proofs (as opposed to any
theoretical benefits).

Kevin, I would like to second Michael's interest in seeing these 20
commutative diagrams. Moreover, I'd also be very interested in seeing
your "spaghetti code" (quote from the slides of your Big Proof talk): it
seems it should be informative to see where your initial approach went
wrong, and how much these problems and their solution had anything to do
at all with the formal system you were working in. Are your original
files perhaps available somewhere?


--

Nicolas




-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fromzerotoinfinity.xyz.