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.
Andrei
