on 9/7/12 5:48 PM, Cris Perdue <[email protected]> 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! > For those who have read this far, I'd very much like to learn what options > there may be for using ML (or I presume OCaml) for building Web > applications. I'm more than happy to discuss the question, but this proof > assistant is going to need to become a Web application, for a number of > reasons. I'm not sure the web application itself would be written in ML, perhaps just the core engine. I suppose it would be nice if it could all be in ML, but I'm afraid I don't know much about that sort of thing. > Going on to your further points, yes I totally agree that getting serious > adoption requires a lot more than just programming of a core engine. In > fact it will require considerable work figuring out how to hide 99.9% of > the complexity from 99% of the users (numbers approximate). ;-) Well this would be a fundamental aspect of the ML program. > Your various comments about requirements sound good to me, including the > issue of limiting jumps in reasoning. Beeson's retrospective paper "Design > Principles of MathPert" ( > http://www.michaelbeeson.com/research/papers/hisc.pdf) I think is well > worth a read. It addresses this and various other issues in educational > math software. He focuses on assisting solution of math problems, but it > his system does rigorous proofs under the hood and the paper seems > perfectly relevant to assisting with proofs of theorems. Thanks very much for this pointer. Someone once mentioned this paper to me before, I seem to remember, but it somehow slipped through the net. This guy is definitely thinking about it in a similar way. I wholeheartedly agree with all of his principles in section 2. Mark. ------------------------------------------------------------------------------ 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
