[28015] in Perl-Users-Digest
Perl-Users Digest, Issue: 9379 Volume: 10
daemon@ATHENA.MIT.EDU (Perl-Users Digest)
Sun Jun 25 18:15:16 2006
Date: Sun, 25 Jun 2006 15:15:08 -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 Sun, 25 Jun 2006 Volume: 10 Number: 9379
Today's topics:
Re: What is Expressiveness in a Computer Language <anton@appsolutions.com>
Re: What is Expressiveness in a Computer Language <cdsmith@twu.net>
Re: What is Expressiveness in a Computer Language <news@andmc.com>
Re: What is Expressiveness in a Computer Language <marshall.spight@gmail.com>
Re: What is Expressiveness in a Computer Language <cdsmith@twu.net>
Re: What is Expressiveness in a Computer Language <news@andmc.com>
Re: What is Expressiveness in a Computer Language <gneuner2/@comcast.net>
Re: What is Expressiveness in a Computer Language rossberg@ps.uni-sb.de
Re: What is Expressiveness in a Computer Language <dnew@san.rr.com>
Re: What is Expressiveness in a Computer Language <cdsmith@twu.net>
Re: What is Expressiveness in a Computer Language <cfc@shell01.TheWorld.com>
Re: What is Expressiveness in a Computer Language <gdr@integrable-solutions.net>
Re: What is Expressiveness in a Computer Language <gdr@integrable-solutions.net>
Re: What is Expressiveness in a Computer Language <david.nospam.hopwood@blueyonder.co.uk>
Digest Administrivia (Last modified: 6 Apr 01) (Perl-Users-Digest Admin)
----------------------------------------------------------------------
Date: Sun, 25 Jun 2006 18:11:22 GMT
From: Anton van Straaten <anton@appsolutions.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <elAng.56441$Lm5.36771@newssvr12.news.prodigy.com>
rossberg@ps.uni-sb.de wrote:
>>>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 language is not a subset, if at all, it's the other way round, but
> I'd say they are rather incomparable. That is, they are different
> languages.
The "subset" characterization is not important for what I'm saying. The
fact that they are different languages is what's important. If you
agree about that, then you can at least understand which language I'm
referring to when I say "latently-typed language".
Besides, many dynamically-typed languages have no formal models, in
which case the untyped formal model I've referred to is just a
speculative construct. The language I'm referring to with
"latently-typed language" is the language that programmers are familiar
with, and work with.
>>That is starting to get a bit too mystical for my tastes.
>
>
> I have to agree.
>
> \sarcasm One step further, and somebody starts calling C a "latently
> memory-safe language", because a real programmer "knows" that his code
> is in a safe subset... And where he is wrong, dynamic memory page
> protection checks will guide him.
That's a pretty apt comparison, and it probably explains how it is that
the software we all use, which relies so heavily on C, works as well as
it does.
But the comparison critiques the practice of operating without static
guarantees, it's not a critique of the terminology.
Anton
------------------------------
Date: Sun, 25 Jun 2006 12:22:13 -0600
From: Chris Smith <cdsmith@twu.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <MPG.1f08823f2d62b6219896fe@news.altopia.net>
Joachim Durchholz <jo@durchholz.org> wrote:
> > The immutability comes from the fact (perhaps implicit in these
> > textbooks, or perhaps they are not really texts on formal type theory)
> > that types are assigned to expressions,
>
> That doesn't *define* what's a type or what isn't!
>
I'm sorry if you don't like it, but that's all there is. That's the
point that's being missed here. It's not as if there's this thing
called a type, and then we can consider how it is used by formal type
systems. A type, in formal type theory, is ANY label that is assigned
to expressions of a program for the purpose of making a formal type
system work. If you wish to claim a different use of the word and then
try to define what is or is not a type, then be my guest. However,
formal type theory will still not adopt whatever restrictions you come
up with, and will continue to use the word type as the field has been
using the word for a good part of a century now.
The first step toward considering the similarities and differences
between the different uses of "type" in dynamic type systems and formal
type theory is to avoid confusing aspects of one field with the other.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
------------------------------
Date: Sun, 25 Jun 2006 19:28:01 +0100
From: Andrew McDonagh <news@andmc.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <e7mkk7$dge$1@news.freedom2surf.net>
Joachim Durchholz wrote:
> Chris Smith schrieb:
>> Joachim Durchholz <jo@durchholz.org> wrote:
>>> Sorry, I have to insist that it's not me who's stretching terms here.
>>>
>>> All textbook definitions that I have seen define a type as the
>>> set/operations/axioms triple I mentioned above.
>>> No mention of immutability, at least not in the definitions.
>>
>> The immutability comes from the fact (perhaps implicit in these
>> textbooks, or perhaps they are not really texts on formal type theory)
>> that types are assigned to expressions,
>
> That doesn't *define* what's a type or what isn't!
>
> If it's impossible to assign types to all expressions of a program in a
> language, that does mean that there's no useful type theory for the
> program, but it most definitely does not mean that there are no types in
> the program.
> I can still sensibly talk about sets of values, sets of allowable
> operations over each value, and about relationships between inputs and
> outputs of these operations.
>
> So programs have types, even if they don't have a static type system.
> Q.E.D.
>
Of course not. Otherwise programs using dynamically typed systems
wouldnt exist.
> Regards,
> Jo
I haven't read all of this thread, I wonder, is the problem to do with
Class being mistaken for Type? (which is usually the issue)
------------------------------
Date: 25 Jun 2006 11:35:04 -0700
From: "Marshall" <marshall.spight@gmail.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <1151260503.976524.77060@b68g2000cwa.googlegroups.com>
Chris F Clark wrote:
> Chris F Clark (I) wrote:
>
> > I'm particularly interested if something unsound (and perhaps
> > ambiguous) could be called a type system. I definitely consider such
> > things type systems.
>
> "Marshall" <marshall.spight@gmail.com> wrote:
>
> > I don't understand. You are saying you prefer to investigate the
> > unsound over the sound?
> ...
> > Again, I cannot understand this. In a technical realm, vagueness
> > is the opposite of understanding.
>
> At the risk of injecting too much irrelevant philosophy into the
> discussion, I will with great trepdiation reply.
I agree this is OT, but I'm not sure about the source of trepidation.
> First in the abstrtact: No, understanding is approximating.
Agreed.
> The world is inherently vague.
Our understanding of the world is vague. The world itself is
not at all vague.
> We make false symbolic models of the world which
> are consistent, but at some level they do not reflect reality,
Yes...
> because reality isn't consistent.
What?!
> Only by abtracting away the inherent
> infinite amout of subtlety present in the real universe can we come to
> comprehensible models.
Sure. (Although I object to "infinite.")
> Those models can be consistent, but they are
> not the universe. The models in their consistency, prove things which
> are not true about the real universe.
Sure, sure, sure. None of these is a reaon to prefer the unsound
over the sound.
> Now in the concrete: In my work productivity is ultimately important.
> Therefore, we live by the 80-20 rule in numerous variations. One of
> ths things we do to achieve productivity is simplify things. In fact,
> we are more interested in an unsound simplification that is right 80%
> of the time, but takes only 20% of the effort to compute, than a
> completely sound (100% right) model which takes 100% of the time to
> compute (which is 5 times as long). We are playing the probabilities.
What you are describing is using a precise mathematical function
to approximate a different precise mathematical function. This
argues for the value of approximation functions, which I do not
dispute. But this does not in any way support the idea of vague
trumping precise, informal trumping formal, or unsoundness as
an end in itself.
> It's not that we don't respect the sound underpining, the model which
> is consistent and establishes certain truths. However, what we want
> is the rule of thumb which is far simpler and approximates the sound
> model with reasonable accuracy. In particular, we accept two types of
> unsoundness in the model. One, we accept a model which gives wrong
> answers which are detectable. We code tests to catch those cases, and
> use a different model to get the right answer. Two, we accept a model
> which gets the right answer only when over-provisioned. for example,
> if we know a loop will occassionaly not converge in the n-steps that
> it theoretically should, we will run the loop for n+m steps until the
> approximation also converges--even if that requires allocating m extra
> copies of some small element than are theoretically necessary. A
> small waste of a small resource, is ok if it saves a waste of a more
> critical resource--the most critical resource of all being our project
> timeliness.
=CE=A5es, I'm quite familiar with modelling, abstraction, approximation,
etc. However nothing about those endevours suggests to me
that unsoundness is any kind of goal.
> Marshall's last point:
>
> > I flipped a coin to see who would win the election; it came
> > up "Bush". Therefore I *knew* who was going to win the
> > election before it happened. See the probem?
>
> Flipping one coin to determine an election is not playing the
> probabilities correctly. You need a plausible explanation for why the
> coin should predict the right answer and a track record of it being
> correct. If you had a coin that had correctly predicted the previous
> 42 presidencies and you had an explanation why the coin was right,
> then it would be credible and I would be willing to wager that it
> could also predict that the coin could tell us who the 44th president
> would be. One flip and no explanation is not sufficient. (And to the
> abstract point, to me that is all knowledge is, some convincing amount
> of examples and a plausible explanation--anyone who thinks they have
> more is appealing to a "knowledge" of the universe that I don't
> accept.)
I used a coin toss; I could also have used a psycic hotline. There
is an explanation for why those things work, but the explanation
is unsound.
> Look at where that got Russell and Whitehead.
Universal acclaim, such that their names will be praised for
centuries to come?
> I'm just trying to be "honest" about that fact and find ways to
> compensate for my own failures.
Limitation !=3D failure.
Marshal
------------------------------
Date: Sun, 25 Jun 2006 12:39:52 -0600
From: Chris Smith <cdsmith@twu.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <MPG.1f0886663b38a0d29896ff@news.altopia.net>
Andrew McDonagh <news@andmc.com> wrote:
> I haven't read all of this thread, I wonder, is the problem to do with
> Class being mistaken for Type? (which is usually the issue)
Hi Andrew!
Not much of this thread has to do with object oriented languages... so
the word "class" would be a little out of place. However, it is true
that the word "type" is being used in the dynamically typed sense to
include classes from class-based OO languages (at least those that
include run-time type features), as well as similar concepts in other
languages. Some of us are asking for, and attempting to find, a formal
definition to justify this concept, and are so far not finding it.
Others are saying that the definition is somehow implicitly
psychological in nature, and therefore not amenable to formal
definition... which others (including myself) find rather unacceptable.
I started out insisting that "type" be used with its correct formal
definition, but I'm convinced that was a mistake. Asking someone to
change their entire terminology is unlikely to succeed. I'm now
focusing on just trying to represent the correct formal definition of
types in the first place, and make it clear when one or the other
meaning is being used.
Hopefully, that's a fair summary of the thread to date.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
------------------------------
Date: Sun, 25 Jun 2006 19:57:51 +0100
From: Andrew McDonagh <news@andmc.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <e7mmc4$en7$1@news.freedom2surf.net>
Chris Smith wrote:
> Andrew McDonagh <news@andmc.com> wrote:
>> I haven't read all of this thread, I wonder, is the problem to do with
>> Class being mistaken for Type? (which is usually the issue)
>
> Hi Andrew!
Hi Chris
>
> Not much of this thread has to do with object oriented languages... so
> the word "class" would be a little out of place.
Glad to here.
> However, it is true
> that the word "type" is being used in the dynamically typed sense to
> include classes from class-based OO languages (at least those that
> include run-time type features), as well as similar concepts in other
> languages. Some of us are asking for, and attempting to find, a formal
> definition to justify this concept, and are so far not finding it.
> Others are saying that the definition is somehow implicitly
> psychological in nature, and therefore not amenable to formal
> definition... which others (including myself) find rather unacceptable.
>
> I started out insisting that "type" be used with its correct formal
> definition, but I'm convinced that was a mistake. Asking someone to
> change their entire terminology is unlikely to succeed. I'm now
> focusing on just trying to represent the correct formal definition of
> types in the first place, and make it clear when one or the other
> meaning is being used.
>
> Hopefully, that's a fair summary of the thread to date.
>
Cheers much appreciated!
Andrew
------------------------------
Date: Sun, 25 Jun 2006 15:33:07 -0400
From: George Neuner <gneuner2/@comcast.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <q7jt92tovq5qci2ei16h437tglltvlssvh@4ax.com>
On Sun, 25 Jun 2006 13:42:45 +0200, Joachim Durchholz
<jo@durchholz.org> wrote:
>George Neuner schrieb:
>> The point is really that the checks that prevent these things must be
>> performed at runtime and can't be prevented by any practical type
>> analysis performed at compile time. I'm not a type theorist but my
>> opinion is that a static type system that could, a priori, prevent the
>> problem is impossible.
>
>No type theory is needed.
>Assume that the wide index type goes into a function and the result is
>assigned to a variable fo the narrow type, and it's instantly clear that
>the problem is undecidable.
Yes ... the problem is undecidable and that can be statically checked.
But the result is that your program won't compile even if it can be
proved at runtime that an illegal value would never be possible.
>Undecidability can always be avoided by adding annotations, but of
>course that would be gross overkill in the case of index type widening.
Just what sort of type annotation will convince a compiler that a
narrowing conversion which could produce an illegal value will, in
fact, never produce an illegal value?
[Other than "don't check this" of course.]
George
--
for email reply remove "/" from address
------------------------------
Date: 25 Jun 2006 12:42:44 -0700
From: rossberg@ps.uni-sb.de
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <1151264564.653872.151090@m73g2000cwd.googlegroups.com>
Joachim Durchholz wrote:
>
> > but (Standard) ML surely has none.
>
> NLFFI?
>
> > Same with Haskell as defined by its spec.
>
> Um... I'm not 100% sure, but I dimly (mis?)remember having read that
> UnsafePerformIO also offered some ways to circumvent the type system.
Neither NLFFI nor unsafePerformIO are official part of the respective
languages. Besides, foreign function interfaces are outside a language
by definition, and can hardly be taken as an argument - don't blame
language A that unsafety arises when you subvert it by interfacing with
unsafe language B on a lower level.
> >> and even C is typesafe unless you use unsafe constructs.
> >
> > Tautology. Every language is "safe unless you use unsafe constructs".
>
> No tautology - the unsafe constructs aren't just typewise unsafe ;-p
>
> That's exactly why I replaced Luca Cardelli's "safe/unsafe"
> "typesafe/not typesafe". There was no definition to the original terms
> attached, and this discussion is about typing anyway.
The Cardelli paper I was referring to discusses it in detail. And if
you look up the context of my posting: it was exactly whether safety is
to be equated with type safety.
> >> IOW from a type-theoretic point of view, there is no real difference
> >> between their typesafe and not typesafe languages in the "statically
> >> typed" column; the difference is in the amount of unsafe construct usage
> >> in practial programs.
> >
> > Huh? There is a huge, fundamental difference: namely whether a type
> > system is sound or not.
>
> I think you're overstating the case.
>
> In type theory, of course, there's no such things as an "almost typesafe
> language" - it's typesafe or it isn't.
Right, and you were claiming to argue from a type-theoretic POV.
[snipped the rest]
- Andreas
------------------------------
Date: Sun, 25 Jun 2006 20:00:25 GMT
From: Darren New <dnew@san.rr.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <tXBng.16192$Z67.12248@tornado.socal.rr.com>
Marshall wrote:
> Also: has subtyping polymorphism or not, has parametric polymorphism or
> not.
And covariant or contravariant.
--
Darren New / San Diego, CA, USA (PST)
Native Americans used every part
of the buffalo, including the wings.
------------------------------
Date: Sun, 25 Jun 2006 14:28:22 -0600
From: Chris Smith <cdsmith@twu.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <MPG.1f089fd357e69ece989700@news.altopia.net>
George Neuner <gneuner2/@comcast.net> wrote:
> >Undecidability can always be avoided by adding annotations, but of
> >course that would be gross overkill in the case of index type widening.
>
> Just what sort of type annotation will convince a compiler that a
> narrowing conversion which could produce an illegal value will, in
> fact, never produce an illegal value?
The annotation doesn't make the narrowing conversion safe; it prevents
the narrowing conversion from happening. If, for example, I need to
subtract two numbers and all I know is that they are both between 2 and
40, then I only know that the result is between -38 and 38, which may
contain invalid array indices. However, if the numbers were part of a
pair, and I knew that the type of the pair was <pair of numbers, 2
through 40, where the first number is greater than the second>, then I
would know that the difference is between 0 and 38, and that may be a
valid index.
Of course, the restrictions on code that would allow me to retain
knowledge of the form [pair of numbers, 2 through 40, a > b] may be
prohibitive. That is an open question in type theory, as a matter of
fact; whether types of this level of power may be inferred by any
tractable procedure so that safe code like this may be written without
making giving the development process undue difficulty by requiring ten
times as much type annotations as actual code. There are attempts that
have been made, and they don't look too awfully bad.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
------------------------------
Date: 25 Jun 2006 17:03:53 -0400
From: Chris F Clark <cfc@shell01.TheWorld.com>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <sdd1wtdymkm.fsf@shell01.TheWorld.com>
Chris F Clark <cfc@shell01.TheWorld.com> (I) wrote:
> Do you reject that there could be something more general than what a
> type theorist discusses? Or do you reject calling such things a type?
Chris Smith <cdsmith@twu.net> wrote:
> I think that the correspondence partly in the wrong direction to
> describe it that way.
...
> What I can't agree to is that what you propose is actually more general.
> It is more general in some ways, and more limited in others. As such,
> the best you can say is that is analogous to formal types in some ways,
> but certainly not that it's a generalization of them.
Yes, I see your point.
Me:
> I'm particularly interested if something unsound (and perhaps
> ambiguous) could be called a type system.
Chris Smith:
> Yes, although this is sort of a pedantic question in the first place, I
> believe that an unsound type system would still generally be called a
> type system in formal type theory. However, I have to qualify that with
> a clarification of what is meant by unsound. We mean that it DOES
> assign types to expressions, but that those types are either not
> sufficient to prove what we want about program behavior, or they are not
> consistent so that a program that was well typed may reduce to poorly
> typed program during its execution. Obviously, such type systems don't
> prove anything at all, but they probably still count as type systems.
Yes, and you see mine.
These informal systems, which may not prove what they claim to prove
are my concept of a "type system". That's because at some point,
there is a person reasoning informally about the program. (There may
also people reasoning formally about the program, but I am going to
neglect them.) It is to the people who are reasoning informally about
the program we wish to communicate that there is a type error. That
is, we want someone who is dealing with the program informally to
realize that there is an error, and that this error is somehow related
to some input not being kept within proper bounds (inside the domain
set) and that as a result the program will compute an unexpected and
incorrect result.
I stressed the informal aspect, because the intended client of the
program is almost universally *NOT* someone who is thinking rigorously
about some mathematical model, but is dealing with some "real world"
phenomena which they wish to model and may not have a completely
formed concrete representation of. Even the author of the program is
not likely to have a completely formed rigorous model in mind, only
some approxiamtion to such a model.
I also stress the informality, because beyond a certain nearly trivial
level of complexity, people are not capable of dealing with truly
formal systems. As a compiler person, I often have to read sections
of language standards to try to discern what the standard is requiring
the compiler to do. Many language standards attempt to describe some
formal model. However, most are so imprecise and ambiguous when they
attempt to do so that the result is only slightly better than not
trying at all. Only when one understands the standard in the context
of typical practice can one begin to fathom what the standard is
trying to say and why they say it the way they do.
A typical example of this is the grammars for most programming
languages, they are expressed in a BNF variant. However, most of the
BNF descriptions omit important details and gloss over certain
inconsistencies. Moreover, most BNF descriptions are totally
unsuitable to a formal translation (e.g. an LL or LR parser generator,
or even an Earley or CYK one). Yet, when considered in context of
typical implementations, the errors in the formal specification can
easily be overlooked and resolved to produce what the standard authors
intended.
For example, a few years ago I wrote a Verilog parser by
transliterating the grammar in the standard (IEEE 1364-1995) into the
notation used by my parser generator, Yacc++. It took a couple of
days to do so. The resulting parser essentially worked on the first
try. However, the reason it did so, is that I had a lot of outside
knowledge when I was making the transliteration. There were places
where I knew that this part of the grammar was lexical for lexing and
this part was for parsing and cut the grammar correctly into two
parts, despite there being nothing in the standard which described
that dichotomy. There were other parts, like the embedded
preprocessor, that I knew were borrowed from C, so that I could use
the reoultions of issues the way a C compiler would do so, to guide
resolving the ambiguities in the Verilog standard. There were other
parts, I could tell the standard was simply written wrong, that is
where the grammar did not specify the correct BNF, because the BNF
they had written did not specifiy something which would make
sense--for example, the endif on an if-then-else-statement was bound
to the else, so that one would write an if then without an endif, but
and if then else with the endif--and I knew that was not the correct
syntax.
The point of the above paragraph is that the very knowledgable people
writing the Verilog standard made mistakes in their formal
specification, and in fact these mistakes made it passed several
layers of review and had been formally ratified. Given the correct
outside knowledge these mistakes are relatively trivial to ignore and
correct. However, from a completely formal perspective, the standard
is simply incorrect.
More importantly, chip designers use knowledge of the standard to
guide the way they write chip descriptions. Thus, at some level these
formal erros, creep into chip designs. Fortunately, the chip
designers also look past the inconsistencies and "program" (design) in
a language which looks very like standard Verilog, but actually says
what they mean.
Moreover, not only is the grammar in the standard a place where
Verilog is not properly formalized. There are several parts of the
type model which suffer similar problems. Again, we have what the
standard specifies, and what is a useful (and expected) description of
the target model. There are very useful and informal models of how
the Verilog language work and what types are involved. There is also
an attempt in the standard to convey some of these aspects formally.
Occassionally, the formal description is write and illuminating, at
other times it is opaque and at still other times, it is inconsistent,
saying contradictory things in different parts of the standard.
Some of the more egregious errors were corrected in the 2001 revision.
However, at the same time, new features were added which were (as far
as I can tell) just as inconsistently specified. And, this is not the
case of incompetence or unprofessionalism. The Verilog standard is
not alone in these problems--it's just my most recent experience, and
thus the one I am most familiar with at the moment.
I would expect the Python, Scheme, Haskell, and ML standards to be
more precise and less inconsistent, because of their communities.
However, I would be surprised if they were entirely unambiguous and
error-free. In general, I think most non-trivial attempts at
formalization flounder on our inability.
Therefore, I do not want to exlcude from type systems, things wich are
informal and unsound. They are simply artifacts of human creation.
-Chris
------------------------------
Date: 26 Jun 2006 00:24:38 +0200
From: Gabriel Dos Reis <gdr@integrable-solutions.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <m3hd28dgbd.fsf@uniton.integrable-solutions.net>
Joachim Durchholz <jo@durchholz.org> writes:
[...]
| (Yes, I'm being silly. But the point is very serious. Even with less
| silly examples, whether a language or subset is "safe" entirely
| depends on what you define to be "safe", and these definitions tend to
| vary vastly across language communities.)
Yes, I know. I hoped we would escape sillyland for the sake of
productive conversation.
-- Gaby
------------------------------
Date: 26 Jun 2006 00:32:01 +0200
From: Gabriel Dos Reis <gdr@integrable-solutions.net>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <m3bqsgdfz2.fsf@uniton.integrable-solutions.net>
rossberg@ps.uni-sb.de writes:
| think that it is too relevant for the discussion at hand. Moreover,
| Harper talks about a relative concept of "C-safety".
Then, I believe you missed the entire point.
First point: "safety" is a *per-language* property. Each language
comes with its own notion of safety. ML is ML-safe; C is C-safe;
etc. I'm not being facetious; I think this is the core of the
confusion.
Safety is an internal consistency check on the formal definition of
a language. In a sense it is not interesting that a language is
safe, precisely because if it weren't, we'd change the language to
make sure it is! I regard safety as a tool for the language
designer, rather than a criterion with which we can compare
languages.
[...]
| Or are you trying to suggest that we should indeed consider C safe for
| the purpose of this discussion?
I'm essentially suggesting "silly arguments" (as noted by someone
in another message) be left out for the sake of productive
conversation. Apparently, I did not communicate that point well enough.
-- Gaby
------------------------------
Date: Sun, 25 Jun 2006 21:36:10 GMT
From: David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
Subject: Re: What is Expressiveness in a Computer Language
Message-Id: <elDng.218638$8W1.61900@fe1.news.blueyonder.co.uk>
Scott David Daniels wrote:
> rossberg@ps.uni-sb.de wrote:
>
>> Huh? There is a huge, fundamental difference: namely whether a type
>> system is sound or not. A soundness proof is obligatory for any serious
>> type theory, and failure to establish it simply is a bug in the theory.
>
> So you claim Java and Objective C are "simply bugs in the theory."
Java's type system was unsound for much of its life. I think that supports
the point that it's inadequate to simply "wish and hope" for soundness,
and that a proof should be insisted on.
--
David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
------------------------------
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 9379
***************************************
