Hello everyone,
I think the two problems Freek mentioned are indeed by far the most
important obstacles to creating a truly usable proof assistant. However,
there is also merit in addressing the points Mark and Cris mention: A nice
system that solves all these "surface" usability issues, may well attract
more users, even if the two core problems remain unsolved. And a "critical
mass" of users can be very helpful in solving the two key problems as well.
Note that I do not mean to imply that Freek's main problems will simply go
away if the user base is large enough. These are deep research problems
that will require new ideas to solve. However, attracting more users and
thus more researchers to the field certainly can't hurt.
To put it differently: As a working mathematician, I'd personally love to
use a "nice proof assistant" that solves all the surface usability issues,
even if the two core problems remain and need many more years to be solved.
Cheers,
Felix
2012/7/13 Cris Perdue <[email protected]>
> Hi Freek,
>
> On Fri, Jul 13, 2012 at 5:32 AM, Freek Wiedijk <[email protected]> wrote:
>
>> Hi Cris,
>>
>> >I was speaking from a software engineering and usability
>> >point of view.
>>
>> Okay, just to fix our minds: would you consider Knuth's/
>> Lamport's latex to be "usable" in this sense? Because I
>> would strongly claim that it is. It's one of the most
>> usable systems I know.
>>
>
> Thanks for asking! Usability is not an absolute, it is relative to the
> user and the purpose. I'm glad you find latex usable as well as useful.
>
> Consider how people may come to use LaTeX. If you are an academic you may
> have a strong motivation to prepare papers for publication. If that means
> investing time and effort to learn LaTeX, you may be willing. If your
> colleagues use it and recommend it, if some conferences or publishers
> require it, all of that might reinforce your readiness to adopt it. If you
> like the payoff, you tend to find it usable.
>
> First-time usability can be crucial for adoption of technology that users
> aren't very convinced that they need or want. (For proof assistants I think
> this might be 99.99% of potential users.) If the potential user tries it
> and gets an immediate feeling of success, he or she is likely to take
> another step. Otherwise most potential users quit and don't come back
> unless maybe a friend starts gushing about how great it is. Then maybe they
> will give it one more try. If the product passes the user's first "sniff
> test", the user still wants to feel that bits of additional effort will pay
> off nicely too.
>
> Most potential users of a new tool such as a proof assistant have some
> other known path toward his or her goal -- pencil and paper or a whiteboard
> for proofs or problem solving; testing for software development;
> computational approximations for engineering. The cost of learning to use
> this proof assistant thing might be high, and the payoff is uncertain.
> People have lots of other things to do. So the tool had better make a very
> good first impression. That is my view, and I think it's a pretty standard
> view on this sort of thing by people who worry about technology adoption.
>
> Maybe this is old news to you, but if so I think it's still worth saying.
>
> Best regards,
> Cris
>
>
>>
>> That's why I think that Mark's focus on things like error
>> messages and concrete syntax is missing the point. Latex is
>> pretty horrible in that respect, but _that doesn't matter._
>>
>> 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
>
>
--
http://www.felixbreuer.net
------------------------------------------------------------------------------
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
