Hi Bill, > I've worked very hard to make my miz3 Hilbert axiomatic geometry code > readable, and taking huge leaps nobody could follow would be > counterproductive. But I'm against shackling the proof assistant, as we agree > Mizar does but miz3 does not: > > Yes, Mizar is certainly shackled in the way Michael described. > > I can't figure out your position. I agree there might be some value in > shackling for retrieval from huge libraries. Why don't we concentrate on > education. I contend that shackling the students' proof assistant is bad > design. Michael did not say this, but I say it after listening to Michael, > and I'm glad that miz3 is not shackling the students (me, right now).
My (current :-) position is that the code in large math libraries should be easy to write, read and maintain. For easy writing, you want the strongest possible AI assistance, for reading you want it transformed into something human-understandable, and for maintenance you want it transformed into something easily checkable by a computer, possibly by robust and predictable algorithms that give you enough feedback when proof checking fails. There are various tensions between these goals and people solve them in various ways, this is research :-). Josef > > -- > Best, > Bill > > ------------------------------------------------------------------------------ > Live Security Virtual Conference > Exclusive live event will cover all the ways today's security and > threat landscape has changed and how IT managers can respond. Discussions > will include endpoint security, mobile security and the latest in malware > threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
