"Andrei Alexandrescu" <seewebsiteforem...@erdani.org> wrote in message
news:i2snsk$1p9...@digitalmars.com...
retard wrote:
I really love digitalmars.D because this is one of the few places where
99% of the community has zero experience with other languages, other
paradigms (non-imperative), automatic theorem provers, or anything not
related to D. There's a whole choir against theorem proving now. The
funniest thing is that none of you seem to have any clue about how those
programs work. Has anyone except the almighty Andrei ever even downloaded
a theorem prover?
From the desk of: Almighty Andrei, New H(e)aven, CT
Almighty Andrei confirms hereby that he tried to used an automated theorem
prover to simplify his Masters thesis work back in 2003. To his shame he
even forgot its name (Coq?) Unfortunately he decided it was too difficult
to set up and use, so he resorted to manual proofs. His MS thesis contains
twenty-something theorems, all proven by hand.
Almighty Andrei wishes to state that his perception of automated theorem
proving is that it can be useful for proving properties of systems as long
as both the properties and the systems are confined enough. For
interesting properties of large systems, theorem proving has notable
scaling difficulties. Also, as Don mentioned, the models used by theorem
provers often abstract away certain realities.
Which does not make the idea "absurd", or "astonishing that it ever had any
traction". What Don said was stupid and ignorant, and you should be honest
enough to say so.
Andrei
