Hi Freek, I agree that these are very very important, but there are certainly other things wrong in my opinion.
Here's a small list of things that are at the top of my head: - lack of exact control of imperative-style commands - lack of support for various styles of proof commonly used on paper (e.g. a "transitive" style) - poor error messages - poor ability to control what is and what is not displayed - poorly designed concrete syntax/pretty printer, that means Pollack Inconsistency becomes a problem - .... there are various other things I can't think of at the moment Note that not every system suffers badly from all of these problems, but in my opinion, every existing system suffers from most. I'm not suggesting that any in my list are individually as important as the two in your list, but sometimes the combination of many small problems is greater than their sum. Sometimes, because of one limitation, the user finds they have to use some less natural technique, and in pursing that they might encounter another problem or two, and it is the combination of these problems that conspire to present to the user a difficult challenge in how to complete a proof that is really quite straightforward on paper. I don't know about other users, but I used to get this all the time. I believe that by making 20 relatively small improvements to usability, the net effect can be a massive jump in usability. Mark on 12/7/12 11:38 AM, Freek Wiedijk <[email protected]> wrote: > Hi Mark, > >>It's just that no-one's done it yet! > > There are just two things that make proof assistants > difficult to use: > > 1. There is not sufficient automation of trivial stuff. > > I.e., you generally need to break down your reasoning into > smaller steps than how you would experience things when > you wouldn't be dealing with a proof assistant. Maybe you > _would_ experience those steps very fleetingly, but you > wouldn't focus at them in the way a proof assistant > forces you to. It's like doing math veeeerrrrryyyy > sllloooowwlllllyyy. > > If some step in a proof is obvious to you, you want to be > able to just say "well, that's obvious" and nothing more. > That's unfortunately not how it seems to work right now. > Even if there's automation in a system that can solve > such a problem, you need to be aware _what_ automation > to invoke. > > 2. You need to be able to find things in a library, or > establish that the thing you think you need is not > there yet. > > And you need to be able to keep your library > well-organised and in sync with the versions of your > systems. Not easy. > > Random example: suppose you want to use Schwarz's > inequality in a proof. So _here's_ your formalisation > that you're working on, and _there's_ the library of your > system. Now what? You will need to give search commands, > or switch windows to look at lists of things you might > need, or try to remember what the lemma was called and > what was its exact shape... it's all irritating overhead. > > And when you prove something you will need to decide > on a name for your new lemma. That's something that's > particularly difficult. > > There are no other reasons proof assistants are difficult. > So will these be the two things you'll be addressing? > > Of course these two things are related. And Sledgehammer > clearly is trying to address these problems. But yes, > it's not fully "done yet". > > Freek > > > ------------------------------------------------------------------------------ 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
