Why don't other programming languages have ranges?

[Andrei Alexandrescu]

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