Why don't other programming languages have ranges?
Andrei Alexandrescu
SeeWebsiteForEmail at erdani.org
Thu Jul 29 13:21:40 PDT 2010
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
More information about the Digitalmars-d
mailing list