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
