Mark wrote: > on 9/7/12 5:48 PM, Cris Perdue <c...@perdues.com> wrote: > > >> .... >> >> What I was talking about though is ease of use of software products, >> and a proof assistant is definitely a software product. To get many >> people to use a software product, especially one that is not just a >> minor variation on one they know, it has to be amazingly simple to >> use. This of course will be a huge challenge for this kind of technology. >> > > Actually I don't think it's particularly difficult to do. It's just that > no-one's done it yet! > > Actually I think it is probably extraordinarily difficult. I recall a comment made about certain sorts of user interfaces (actually it was about GUIs but I think equally applicable to a certain style or philosophy of designing user interfaces for complicated software), that they "make easy tasks easy and difficult tasks impossible".
Theorem proving is a difficult task - or, more to the point - when you break it down into its myriad of subtasks, they are all different. The tool that does them all will not be "amazingly simple to use" Jeremy ------------------------------------------------------------------------------ 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
