[PRL] dijkstra anecdote

Eli Barzilay eli at barzilay.org
Fri Dec 5 18:12:09 EST 2003


I think that the basic idea for this is using tactics to describe
refinments -- but even with this, formalizing useful stuff is
extremely heavy.  It's really no wonder mathematicians are so
informal, but eventually the hope is that things like Nuprl will help
in making formal arguments more feasible.

(But talking about argumenting with humans, using formality will only
help you to arrive faster to the core of the argument that is usually
based on vague opinions etc.)

On Dec  5, Matthias Felleisen wrote:
> Nuprl is based and inspired by this whole idea. -- Matthias
> 
> On Friday, December 5, 2003, at 11:45 AM, David A. Herman wrote:
> 
> > More specifically, in EWD 1298, Dijkstra quotes E.T.Bell paraphrasing
> > Leibniz (how's *that* for primary sources?) in his desire for
> >
> >> a general method in which all truths of the reason would be reduced
> >> to a kind of calculation. At the same time this would be a sort of
> >> universal language or script, but infinitely different from all those
> >> projected hitherto; for the symbols and even the words in it would
> >> direct reason; and errors, except those of fact, would be mere
> >> mistakes in calculation.
> >
> > In other words, a formal logic calculus that would apply to all 
> > reasoning about all topics ever. I remember reading somewhere that 
> > Leibniz had this futurist image where, whenever people disagreed about 
> > anything, they'd just write down the propositions involved in the 
> > argument in the symbols of the formal language, push the symbols 
> > around until they came to a conclusion, and then the argument would be 
> > resolved.
> >
> > Dave

-- 
          ((lambda (x) (x x)) (lambda (x) (x x)))          Eli Barzilay:
                  http://www.barzilay.org/                 Maze is Life!


More information about the PRL mailing list