On 27/01/18 23:04, Cris Perdue wrote: > Well no. If a person has neither special preparation nor interest, I would > not wish to bother them.
If you are willing to take a request from me, please do not use “they” as singular. In English, “he” is the canonical generic singular. Although “they” has some historical precedent (so does “thou”, but people rarely use it nonetheless) as a singular, in our time it is part of the ultraliberals' attempt to redefine the language for their political agenda. > On the other hand, I do believe that it is possible for a sufficiently > well-engineered proof assistant to become useful to students with much less > special preparation than is required today, but the possibilities and > tradeoffs would be a complex discussion. If you want to share the difficulties you had while trying to learn HOL Light I will be glad to write documentation for the counterpart in HOL4 if required. That being said, I believe that HOL4 (HOL Light is very similar) is already close to being as simple as possible to learn. The difficulty resides mostly in the prerequisite of knowing formal logic, mathematics and some computer programming, but I believe this is inherent to computer-verified proofs.
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
