Weblogs Forum - Authors and Computer Scientists Scared of Definitions?

Articles |
News |
Weblogs |
Books |
Forums

Artima Forums | Articles | Weblogs | Java Answers | News

Sponsored Link •

Weblogs Forum
Authors and Computer Scientists Scared of Definitions?

53 replies on 4 pages. Most recent reply: Sep 15, 2006 11:09 AM by Mumtaz Shah

Welcome Guest
Sign In

Back to Topic List

Reply to this Topic

Search Forum

Threaded View


Previous Topic		Next Topic

Flat View: This topic has 53 replies on 4 pages [ « | 1 2 3 4 ]

Michael Feathers

Posts: 448
Nickname: mfeathers
Registered: Jul, 2003

Re: Authors and Computer Scientists Scared of Definitions?

Posted: Sep 11, 2006 8:29 AM

> > If you had a definition for 'type' how would you act
> > differently?
>
> When he communicates with other computer scientists, he
> uses the accepted definition and assumes they are also
> using that definition. This facilitates understanding.
> I'm not sure why this desire is considered questionable
> e by so many. Physicists and other scientists would never
> consider using terms that are not clearly defined in
> technical discussions or documents. Pretty much the first
> topic in any introductory Physics course is the exact
> definition of 'mass' and the distinction between mass and
> weight.

The problem with 'type' is that it came about too early in computer science. While one school was busy defining properties of data types (keyword: data) at compile time, another school was defining computation in terms of behavior at runtime, in systems that the other school would think of as 'typeless.'

It's an understandable muddle.

Part of me feels that types aren't fundamental in any sense. They are simply a reasoning tool for one particular paradigm of programming.

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: Authors and Computer Scientists Scared of Definitions?

Posted: Sep 11, 2006 8:59 AM

> Part of me feels that types aren't fundamental in any
> sense. They are simply a reasoning tool for one
> particular paradigm of programming.

I still don't see why it wouldn't be advantageous for the term to be defined within the context of that paradigm.

Max Lybbert

Posts: 314
Nickname: mlybbert
Registered: Apr, 2005

Re: Authors and Computer Scientists Scared of Definitions?

Posted: Sep 11, 2006 2:44 PM

/* Eivind Eklund: I firmly believe that most of the time, the cost of the type declarations (in terms of programmer attention) is not worth it.
*/

/* James Watson: Assuming this is true, is saying that [whether a program will halt] could be determined by a type system the same as saying that halting is a type?
*/

No, but it is possible to determine that the program's use of types is incorrect and can lead to halting.

/* I can come up with some other possible 'properties' of a program: correct, efficient, backwards-compatible, multi-platform, beta, production-ready, state-of-the-art, exciting, boring, annoying...
*/

And while those may not be types, in many cases a type system can help you reason about those properties (backwards compatible, search for "Mr. Rogers" in http://www.joelonsoftware.com/printerFriendly/articles/fog0000000036.html "The code will be factored to use two interfaces: V1 and V2. ... V1::Save can handle the backwards compatibility while V2::Save can be used to save all the new stuff. If you've opened a V1 file and try to use V2 functionality, the program can warn you right away, and you will have to either convert the file or give up the new functionality.")

So far I like Vesa's definition, that a type defines data and the accepted operations on data. You may choose to go through a language mechanism to create a type, or you may simply decide to use

int

s, and outlaw multiplcation by management fiat. You could even go with a dynamically-typed system. Regardless, you've got the data and you've got the acceptable operations. And armed with those two, you can reason better about what you're doing.

Achilleas Margaritis

Posts: 674
Nickname: achilleas
Registered: Feb, 2005

Re: Authors and Computer Scientists Scared of Definitions?

Posted: Sep 12, 2006 3:06 AM

> > To me, Godel's theorem of incompleteness is the root
> cause
> > of errorism !
>
> Could you elaborate on why you think so?

It's simple, really: nothing can be proven until it happens.

This has a foundamental effect on programming: algorithms can not be mechanically proven correct.

Terje Slettebø

Posts: 205
Nickname: tslettebo
Registered: Jun, 2004

Re: Authors and Computer Scientists Scared of Definitions?

Posted: Sep 13, 2006 1:35 PM

> > > To me, Godel's theorem of incompleteness is the root
> > cause
> > > of errorism !
> >
> > Could you elaborate on why you think so?
>
> It's simple, really: nothing can be proven until it
> happens.
>
> This has a foundamental effect on programming: algorithms
> can not be mechanically proven correct.

Well, some people claim to have done that:

"A Mechanized Program Verifier" (http://www.cs.utexas.edu/users/moore/publications/zurich-position.pdf):

"The theorem prover is designed to operate automatically once a conjecture is posed to it. Its behavior is determined by previously proved theorems residing in its database.
[...]
Progress So Far ... 1970–1979: fully automatic proof of insertion sort, including the permutation property, and fully automatic proofs of many other theorems about Pure Lisp programs [3]; the correctness of a McCarthy-Painter-like expression compiler, the soundness and completeness of a propositional tautology checker, and the correctness of the Boyer-Moore fast string searching algorithm in FORTRAN 77..."

Ironically, it has also been used to prove Gödel's first incompleteness theorem.

However, the "holy grail" of program verification may be something of a red herring: If the proofs are way more complex than the program - unless it's automated (and assuming the proof-machine is correct (!)) - how can we know we haven't made an error in the proof...?

In the famous words of Don Knuth:

"Beware of bugs in the above code; I have only proved it correct, not tried it."

Mumtaz Shah

Posts: 10
Nickname: mumtaz
Registered: Feb, 2006

Re: Authors and Computer Scientists Scared of Definitions?

Posted: Sep 14, 2006 12:01 PM

> > > > To me, Godel's theorem of incompleteness is the
> root
> > > cause
> > > > of errorism !
> > >
> > > Could you elaborate on why you think so?
> >
> > It's simple, really: nothing can be proven until it
> > happens.
> >
> > This has a foundamental effect on programming:
> algorithms
> > can not be mechanically proven correct.
>
> Well, some people claim to have done that:
>
> "A Mechanized Program Verifier"
> (http://www.cs.utexas.edu/users/moore/publications/zurich-p
> osition.pdf):
>
> "The theorem prover is designed to operate automatically
> once a conjecture is posed to it. Its behavior is
> determined by previously proved theorems residing in its
> database.
> [...]
> Progress So Far ... 1970–1979: fully automatic proof of
> insertion sort, including the permutation property, and
> fully automatic proofs of many other theorems about Pure
> Lisp programs [3]; the correctness of a
> McCarthy-Painter-like expression compiler, the soundness
> and completeness of a propositional tautology checker, and
> the correctness of the Boyer-Moore fast string searching
> algorithm in FORTRAN 77..."
>
> Ironically, it has also been used to prove Gödel's first
> incompleteness theorem.
>
> However, the "holy grail" of program verification may be
> something of a red herring: If the proofs are way more
> complex than the program - unless it's automated (and
> assuming the proof-machine is correct (!)) - how can we
> know we haven't made an error in the proof...?
>
> In the famous words of Don Knuth:
>
> "Beware of bugs in the above code; I have only proved it
> correct, not tried it."

You asked me: "Could you elaborate on why you think so?"
I said: "No".

Terje Slettebø

Posts: 205
Nickname: tslettebo
Registered: Jun, 2004

Re: Authors and Computer Scientists Scared of Definitions?

Posted: Sep 15, 2006 2:46 AM

> > > > > To me, Godel's theorem of incompleteness is the
> > root
> > > > cause
> > > > > of errorism !
> > > >
> > > > Could you elaborate on why you think so?
> > >
> > > It's simple, really: nothing can be proven until it
> > > happens.
> > >
> > > This has a foundamental effect on programming:
> > algorithms
> > > can not be mechanically proven correct.
> >
> > Well, some people claim to have done that:
> >
> > "A Mechanized Program Verifier"
> >
> (http://www.cs.utexas.edu/users/moore/publications/zurich-p
>
> > osition.pdf):
> >
> > "The theorem prover is designed to operate
> automatically
> > once a conjecture is posed to it. Its behavior is
> > determined by previously proved theorems residing in
> its
> > database.
> > [...]
> > Progress So Far ... 1970–1979: fully automatic proof of
> > insertion sort, including the permutation property, and
> > fully automatic proofs of many other theorems about
> Pure
> > Lisp programs [3]; the correctness of a
> > McCarthy-Painter-like expression compiler, the
> soundness
> > and completeness of a propositional tautology checker,
> and
> > the correctness of the Boyer-Moore fast string
> searching
> > algorithm in FORTRAN 77..."
> >
> > Ironically, it has also been used to prove Gödel's
> first
> > incompleteness theorem.
> >
> > However, the "holy grail" of program verification may
> be
> > something of a red herring: If the proofs are way more
> > complex than the program - unless it's automated (and
> > assuming the proof-machine is correct (!)) - how can we
> > know we haven't made an error in the proof...?
> >
> > In the famous words of Don Knuth:
> >
> > "Beware of bugs in the above code; I have only proved
> it
> > correct, not tried it."
>
> You asked me: "Could you elaborate on why you think so?"
> I said: "No".

Yes, so I noticed, and that wasn't really helpful, so another chimed in with his opinion on the matter. In particular, it wasn't clear whether you _could't_ (as in being able to) or _wouldn't_ (as in not wanting to) elsaborate.

In other words, from your reply, it wasn't at all clear that you even knew what you were talking about, or just threw out something that you presumed sounded clever... (but which may be nonsense) That still isn't clear.

Alex Stojan

Posts: 95
Nickname: alexstojan
Registered: Jun, 2005

Re: Authors and Computer Scientists Scared of Definitions?

Posted: Sep 15, 2006 8:14 AM

> > You asked me: "Could you elaborate on why you think
> so?"
> > I said: "No".

> Yes, so I noticed, and that wasn't really helpful, so
> another chimed in with his opinion on the matter. In
> particular, it wasn't clear whether you _could't_ (as in
> being able to) or _wouldn't_ (as in not wanting to)
> elsaborate.
>
> In other words, from your reply, it wasn't at all clear
> that you even knew what you were talking about, or just
> threw out something that you presumed sounded clever...
> (but which may be nonsense) That still isn't clear.

I'm guessing the answer was: "No (I COULD not)", rather than "No (I don't want to)". Anyway, not very helpful in either case. If someone can't explain why they think so the only explanation is that they don't know what they're talking about.

Mumtaz Shah

Posts: 10
Nickname: mumtaz
Registered: Feb, 2006

Re: Authors and Computer Scientists Scared of Definitions?

Posted: Sep 15, 2006 11:09 AM

I think I threw out something that I "presumed sounded clever". I could not elaborate further because I was not sure what I was talking about. Later I was afraid that my little "No" wasnt noticed and appreciated enough .

My sincerest apologies to Godel. I feel sympathy for him.

Flat View: This topic has 53 replies on 4 pages [ « | 1 2 3 4 ]

Previous Topic

Next Topic