[28007] in Perl-Users-Digest
Perl-Users Digest, Issue: 9371 Volume: 10
daemon@ATHENA.MIT.EDU (Perl-Users Digest)
Sat Jun 24 18:10:17 2006
Date: Sat, 24 Jun 2006 15:10:05 -0700 (PDT)
From: Perl-Users Digest <Perl-Users-Request@ruby.OCE.ORST.EDU>
To: Perl-Users@ruby.OCE.ORST.EDU (Perl-Users Digest)
Perl-Users Digest Sat, 24 Jun 2006 Volume: 10 Number: 9371
Today's topics:
Re: What is Expressiveness in a Computer Language <cfc@shell01.TheWorld.com>
Re: What is Expressiveness in a Computer Language <pc@p-cos.net>
Re: What is Expressiveness in a Computer Language <anton@appsolutions.com>
Re: What is Expressiveness in a Computer Language <cfc@shell01.TheWorld.com>
Re: What is Expressiveness in a Computer Language <cdsmith@twu.net>
Digest Administrivia (Last modified: 6 Apr 01) (Perl-Users-Digest Admin)
----------------------------------------------------------------------
Date: 24 Jun 2006 15:11:58 -0400
From: Chris F Clark <cfc@shell01.TheWorld.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <sddac82bc75.fsf@shell01.TheWorld.com>
Chris Smith <cdsmith@twu.net> writes:
> I thought about this in the context of reading Anton's latest post to
> me, but I'm just throwing out an idea.
I think there is some sense of convergence here. In particular, I
reason about my program using "unsound types". That is, I reason
about my program using types which I can (at least partially)
formalize, but for which there is no sound axiomatic system. Now,
these types are locally sound, i.e. I can prove properties that hold
for regions of my programs. However, the complexity of the programs
prevent me from formally proving the entire program is correct (or
even entirely type-safe)--I generally work in a staticly, but
weakly-typed language. Sometimes, for performance reasons, the rules
need to be bent--and the goal is to bend the rules, but not break
them. At other times, I want to strenghten the rules, make parts of
the program more provably correct.
How does this work in practice? Well, there is a set of ideal types,
I would like to use in my program. Those types would prove that my
program is correct. However, because there are parts of the program
that for perfomnace reasons need me to widen the ideal types to
something less tight, pragmatic types. The system can validate that I
have not broken the pragmatic types. That is not tight enough to
prove the program correct, but it provides some level of security.
To improve my confidence in the program, I borrow the tagging concept
to supplement the static type system. At key points in the program I
can check the type tag to ensure that the data being manipulated
actual matches the unprovable ideal type system. If it doesn't, I
have a witness to the error in my reasoning. It is not perfect, but
it is better than nothing.
Why am I in this state, because I believe that most interesting
programs are beyond my ability to formally prove them, or at least
prove them in "reasonable" time bounds. Therefore, I prove
(universally quantify) some properties of my programs, but many other
(and most of the "interesting") properties, I can only existentially
quantify--it worked in the cases that it was tested on. It is a
corrolary of this, that most programs have bugs--places where the
formal reasoning was incomplete (did not reason down to relevant
interesting property) and the informal reasoning was wrong.
Thus, the two forms of reasoning, static typing to check the formal
properties that it can, and dynamic tagging to catch the errors that
it missed work like a belt and suspenders system. I would like the
static type system to catch more errors, but I need it to express more
to do so, and many of the properties that are interesting require
n-squared operations to validate. Equally important, the dynamic tags
help when working in an essentially untrustworthy world. Not only do
our own programs have bugs, so do the systems we run them on, both
hardware and software. Moreover, alpha radiation and quantum effects
can change "constants" in a program (some of my work has to do with
soft-error rates on chips where we are trying to guarantee that the
chip will have a reasonable MBTF for certain algorithms). That's not
to ignore the effects of malware and other ways your program can be
made less reliable.
Yes, I want a well-proven program, but I also want some guarantee that
the program is actually executing the algorithm specified. That
requires a certain amount of "redundant" run-time checks. Knuth had a
quote about a program only being proven and not tested that reflects
the appropriate cynicism.
I consider any case where a program gives a function outside of its
domain a "type error", because an ideal (but unacheivable) type system
would have prevented it. That does not make all errors, type errors,
because if I give a program an input within its domain and it
mis-computes the result, that is not a type error.
-Chris
------------------------------
Date: Sat, 24 Jun 2006 21:17:06 +0200
From: Pascal Costanza <pc@p-cos.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <4g5hdiF1lpuniU1@individual.net>
Marshall wrote:
> Anton van Straaten wrote:
>> But beyond that, there's an issue here about the definition of "the
>> language". When programming in a latently-typed language, a lot of
>> action goes on outside the language - reasoning about static properties
>> of programs that are not captured by the semantics of the language.
>>
>> This means that there's a sense in which the language that the
>> programmer programs in is not the same language that has a formal
>> semantic definition. As I mentioned in another post, programmers are
>> essentially mentally programming in a richer language - a language which
>> has informal (static) types - but the code they write down elides this
>> type information, or else puts it in comments.
>>
>> We have to accept, then, that the formal semantic definitions of
>> dynamically-checked languages are incomplete in some important ways.
>> Referring to those semantic definitions as "the language", as though
>> that's all there is to the language in a broader sense, is misleading.
>>
>> In this context, the term "latently-typed language" refers to the
>> language that a programmer experiences, not to the subset of that
>> language which is all that we're typically able to formally define.
>
> That is starting to get a bit too mystical for my tastes.
To paraphrase Abelson & Sussman: Programs must be written for people to
read, and only incidentally for compilers to check their types.
;)
Pascal
--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/
------------------------------
Date: Sat, 24 Jun 2006 19:25:11 GMT
From: Anton van Straaten <anton@appsolutions.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <rkgng.157632$F_3.137561@newssvr29.news.prodigy.net>
Marshall wrote:
> Anton van Straaten wrote:
>
>>But beyond that, there's an issue here about the definition of "the
>>language". When programming in a latently-typed language, a lot of
>>action goes on outside the language - reasoning about static properties
>>of programs that are not captured by the semantics of the language.
>>
>>This means that there's a sense in which the language that the
>>programmer programs in is not the same language that has a formal
>>semantic definition. As I mentioned in another post, programmers are
>>essentially mentally programming in a richer language - a language which
>>has informal (static) types - but the code they write down elides this
>>type information, or else puts it in comments.
>>
>>We have to accept, then, that the formal semantic definitions of
>>dynamically-checked languages are incomplete in some important ways.
>>Referring to those semantic definitions as "the language", as though
>>that's all there is to the language in a broader sense, is misleading.
>>
>>In this context, the term "latently-typed language" refers to the
>>language that a programmer experiences, not to the subset of that
>>language which is all that we're typically able to formally define.
>
>
> That is starting to get a bit too mystical for my tastes.
It's informal, but hardly mystical. The formal semantic definitions of
dynamically-checked languages I'm referring to are the typical "untyped"
definitions, in which the language has a single static type.
This means that when you as a programmer see a function that you "know"
e.g. takes a number and returns a number, that knowledge is not
something that's captured by the language's formal semantics or static
type system. All that can be expressed in the language's static type
system is that the function takes a value and returns a value.
When you're programming in your favorite dynamically-typed language,
I'll bet that you're not thinking of functions, or other expressions, in
such a restricted way. Your experience of programming in the language
thus relies heavily on features that are not a "property of the
language", if "the language" is taken to mean its formal semantic
definition.
So in referring to a language as latently-typed, the word "language" can
be taken to mean what a programmer thinks of as the language, rather
than a formal definition that only captures a subset of what the
programmer routinely deals with.
If we don't acknowledge this distinction between the part of the
language that we can capture formally and the part that we haven't
(yet), then we'll be forever stuck without accepted terminology for the
informal bits, because such terminology can always be objected to on the
grounds that it isn't supported by formal semantics.
Anton
------------------------------
Date: 24 Jun 2006 15:34:54 -0400
From: Chris F Clark <cfc@shell01.TheWorld.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <sddac82xs81.fsf@shell01.TheWorld.com>
Chris Smith <cdsmith@twu.net> writes:
> I thought about this in the context of reading Anton's latest post to
> me, but I'm just throwing out an idea.
I wrote:
> I think there is some sense of convergence here.
Apologies for following-up to my own post, but I forgot to describe
the convergence.
The convergence is there is something more general that what type
theorists talk about when discussing types. Type theory is an
abstraction and systemization of reasoning about types. This more
general reasoning doesn't need to be sound, it just needs to be based
aound "types" and computations.
My own reasoning uses such an unsound system. It has clear roots in
sound reasoning, and I wish I could make it sound, but....
In any case, dynamic tagging helps support my unsound reasoning by
providing evidence when I have made an error.
I hope this makes it less mystical for Marshall.
-Chris
------------------------------
Date: Sat, 24 Jun 2006 14:03:14 -0600
From: Chris Smith <cdsmith@twu.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <MPG.1f074872ce4e876e9896f7@news.altopia.net>
Chris F Clark <cfc@shell01.TheWorld.com> wrote:
> Chris Smith <cdsmith@twu.net> writes:
> > I thought about this in the context of reading Anton's latest post to
> > me, but I'm just throwing out an idea.
>
> I wrote:
> > I think there is some sense of convergence here.
>
> Apologies for following-up to my own post, but I forgot to describe
> the convergence.
>
> The convergence is there is something more general that what type
> theorists talk about when discussing types. Type theory is an
> abstraction and systemization of reasoning about types. This more
> general reasoning doesn't need to be sound, it just needs to be based
> aound "types" and computations.
Unfortunately, I have to again reject this idea. There is no such
restriction on type theory. Rather, the word type is defined by type
theorists to mean the things that they talk about. Something becomes a
type the instant someone conceives of a type system that uses it. We
could try to define a dynamic type system, as you seem to say, as a
system that checks against only what can be known about some ideal type
system that would be able to prove the program valid... but I
immediately begin to wonder if it would ever be possible to prove that
something is a dynamic type system for a general-purpose (Turing-
complete) language.
If you could define types for a dynamic type system in some stand-alone
way, then this difficulty could be largely pushed out of the way,
because we could say that anything that checks types is a type system,
and then worry about verifying that it's a sound type system without
worrying about whether it's a subset of the perfect type system. So
back to that problem again.
You also wrote:
> I consider any case where a program gives a function outside of its
> domain a "type error", because an ideal (but unacheivable) type system
> would have prevented it. That does not make all errors, type errors,
> because if I give a program an input within its domain and it
> mis-computes the result, that is not a type error.
So what is the domain of a function? (Heck, what is a function? I'll
neglect that by assuming that a function is just an expression;
otherwise, this will get more complicated.) I see three possible ways
to look at a domain.
(I need a word here that implies something like a set, but I don't care
to verify the axioms of set theory. I'm just going to use set. Hope
that's okay.)
1. The domain is the set of inputs to that expression which are going to
produce a correct result.
2. The domain is the set of inputs that I expected this expression to
work with when I wrote it.
3. The domain is the set of inputs for which the expression has a
defined result within the language semantics.
So the problem, then, more clearly stated, is that we need something
stronger than #3 and weaker than #1, but #2 includes some psychological
nature that is problematic to me (though, admittedly, FAR less
problematic than the broader uses of psychology to date.)
Is that a fair description of where we are in defining types, then?
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
------------------------------
Date: 6 Apr 2001 21:33:47 GMT (Last modified)
From: Perl-Users-Request@ruby.oce.orst.edu (Perl-Users-Digest Admin)
Subject: Digest Administrivia (Last modified: 6 Apr 01)
Message-Id: <null>
Administrivia:
#The Perl-Users Digest is a retransmission of the USENET newsgroup
#comp.lang.perl.misc. For subscription or unsubscription requests, send
#the single line:
#
# subscribe perl-users
#or:
# unsubscribe perl-users
#
#to almanac@ruby.oce.orst.edu.
NOTE: due to the current flood of worm email banging on ruby, the smtp
server on ruby has been shut off until further notice.
To submit articles to comp.lang.perl.announce, send your article to
clpa@perl.com.
#To request back copies (available for a week or so), send your request
#to almanac@ruby.oce.orst.edu with the command "send perl-users x.y",
#where x is the volume number and y is the issue number.
#For other requests pertaining to the digest, send mail to
#perl-users-request@ruby.oce.orst.edu. Do not waste your time or mine
#sending perl questions to the -request address, I don't have time to
#answer them even if I did know the answer.
------------------------------
End of Perl-Users Digest V10 Issue 9371
***************************************
