Why don't other programming languages have ranges?

Jim Balter Jim at Balter.name
Mon Aug 2 23:40:21 PDT 2010


"Andrei Alexandrescu" <SeeWebsiteForEmail at erdani.org> wrote in message 
news:i2snsk$1p93$1 at 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 



More information about the Digitalmars-d mailing list