In Greek, yes. But in English it's usually just "lemmas".
Unless you're like me (and lots of other geeks) and like to use exotic word forms for the fun of it. My dictionary gives both forms, but you're probably the first person (other than myself) whom I've ever heard using the -ta form.
> but the biggest problem (as I see it) is that there is lots and lots of code which does not really lend itself to easy proof (e.g. timing-dependant networking code, GUI code, parallel/distributed code, etc.).
I've never seen proof work for GUIs, but there are methods for doing proofs for time-dependent and/or distributed programs.
> You don't have to provide formal proofs of all code. I would estimate 90% of all array accesses could be done without any run-time checking if...
I'm not so sure run-time checking is such a bad thing. Sure it adds a bit over overhead, but we have a very wrong fixation on performance over correctness. IMO correctness should always be more important than performance. If your boss puts more emphasis on speed than on correctness, just turn in a "Hello World!" program for every project: programs don't get much faster, and BFD if the output wasn't what your boss wanted -- it's just a bug!
Besides, in most cases run-time checking is going to impact performance far less than the inefficient algorithms people tend to use. I shudder at some of the programs I've had to repair because the people who wrote them didn't know the advantages of the most rudimentary data structures, such as trees, in many common circumstances.
> I've rarely had to "work against" strong type systems in the past. Sufficiently expressive type systems are important for this to make sense, I'll admit that; it requires a certain kind of thinking to be able to make use of strong typing effectively. This restriction on "free thought" may be what people find most offensive, but I'm not sure.
That is also my experience, and my perception of why people don't like it.
Strong typing does seem like "a lot of extra keystrokes" and a lot of extra chains on your behavior when you first start using it (no, I'm talking about strong typing, not what passes for that in C++). But after you get used to it you find yourself creating very sophisticated abstract data types and thinking of them as abstractions, so that the programming end becomes very simple and elegant -- as well as completely eliminating certain kinds of bugs that programmers waste an incredible amount of time fighting.
I try to get people to think of strong static typing as a form of constraint-based programming. All a strong type definition actually does is put some constraints on the values a variable or parameter can have. And it's a nifty kind of constraint, because you specify it once rather than all through your code, and because it can be checked at compile time rather than at run time.
> But, at the same time, I truly hope that mechanisms for proving properties about programs will become not only more powerful, but also more widespread.
I also am a fan of formal verification. Unfortunately, formal verification requires a formal specification (to be prove to have been implemented correctly), and once you get to complex application programs (rather than, say, just a sorting routine), providing a correct formal specifications is probably going to approximately as difficult as writing correct programs is now. IOW, it just moves the problem somewhere else.
> > They are less efficient, just as BASIC or C is less efficient than pure assembler,
> They are _NOT_ less efficient. Depending, of course, on your definition of 'efficient': CPU-efficient or Programmer-time-efficient?
I hear that even in terms of CPU-efficiency, some optimizers produce code that runs faster than what humans would write in assembly language in practice.
Semantically, strings are more or less a subset of lists in which the elements are characters. So why do you need a separate data type? You don't, really. Strings only exist for efficiency.
> i think strings mainly exist because of usability considerations - from the developers point of view. they provide a compact notation for "list of characters". furthermore, most languages come with string routines/classes/operators that are a lot more powerful and flexible than their list-equivalent.
He's simply wrong on this one. A list is a data structure, so strings are only a special kind of list if you choose to implement them that way.
In terms of pure abstraction, both strings and list can be thought of as "finite sequences". But strings and lists are not used the same way by programmers (or other people), so there's absolutely no reason to presuppose that they should both be implemented the same way.
In fact I would go further (away from him) and say that the common paradigm of treating strings as arrays of characters is poor design as well. Arrays probably are the best way to implement strings, but from the language design POV they should IMO be treated as a distinctive data type of their own, with native support for the most natural operations and whatever underlying interface works best.
Notice that I say that as a fan of s-expressions. Some of us draw a line between "fan" and "fanatic".
> Why is it, if a Leftist politcal agenda is advanced in a work of "art", the creators are credited with depth, greatness, and strength of character, and yet when a Rightist political agenda is advanced, the creators are jingoist, reactionary, and fascist?
Maybe because artists tend to be leftist, so that most rightist "art" must perforce be made by someone other than artists?
> What part of "The 3-person team from North Vancouver, Canada" did you not read? Anime, in the terms commonly used by American fanboys, refers to Japanese Animation.
This is canime?
Re: I wouldn't read too far into this article...
on
The Hundred-Year Language
·
· Score: 2, Informative
> And he considers something like Object-Oriented Programming a slow evolution?
When you consider that it is just a metaphor for refinements of pre-existing ideas such as data hiding, which in turn are refinements of pre-existing ideas such as structured programming, which in turn are refinements of pre-existing ideas such as "high level" programming languages,...yes, it has been a slow evolution.
> When you are building any formal system you have to start with a set of Axioms. If you throw out the Axiom "people think" what do you have to go on? In essence by throwing out the axiom, you are setting up a situation where anything could be considered thinking, because there is no foundation to compare it with.
Science isn't a formal system; it doesn't have axioms. We have to do as best we can simply by looking to see what happens and then trying to understand it.
So we have this notion that "people think", and we have a very vague notion of what "think" means. Where do we go from there? If we start with the notion that thought is something special that can't arise from mechanical processes, we've answered our question by fiat.
But some of us would like to understand how thinking works rather than having an ex cathedra pronouncement that sets it outside of science from the get go. And everything we've learned about the body, the brain, neurons, neurotransmitters, indicates that humans are just big complex machines with no special ingredients. And in the past few centuries we've made marvelous progress at understanding how these components work, with never a need to invoke the supernatural, metaphysical, etc., yet.
So our question for Searle and his ilk is, what the heck is this human "understanding" if not the result of mechanical processes? If it's not the result of mechanical processes, we'd like to see some evidence for that. If it is the result of mechanical processes, why can't it be done in a computer instead of a bag of dirty water?
Searle's argument is just slight of hand to obscure the basic issues, and buying in to his argument requires accepting an 'axiom' that has no empirical support whatsoever, namely that "understanding" is something special that lies outside the mechanical operation of rules. Essentially he assumes his desired conclusion; everything else is just leaves raked over the path to hide its circularity.
> I don't need that. My second-hand vending machine is sitting there between my theater-style popcorn popper and the second-hand soda fountain I made after reading about it on Slashdot yesterday.
> I have all the major food groups -- sugar, salt, fat, and cholesterol -- all within reach of my computer!
Stop, stop! You're making me hungry! Now I want to run see a movie so I can get some of that popcorn dripping with fake butter.
> Someone noticed this and placed a bet for the same numbers for the first game of day 3, and won the jackpot. As it turns out, the programmer had reset the "FOR day IN..." loop, meaning the first results of each day were the same.
Were "someone" and "the programmer" by chance the same person?
> Back in my SCA days, one local sword maker described how he did it. He started with blanks intended for use as auto leaf springs. After suitable grinding, he had them heat treated. This was Cleveland when it had steel mills. He went to a heat treating shop, handed over the sword blade, said "ASTM Process 50, 4 hours". They said "It'll be ready Thursday".
You mean, all those years I spent quenching my swords in the flowing blood of one-eyed transvestite lumberjacks of royal ancestry, and I would have done just as well taking them down to Edgar's Cut-Rate Annealing in batches of fifty?
> Or, consider the fact that Senate Bill 742 in Oregon, introduced by Republican John Minnis, would define as a terrorist, a person who "plans or participates in an act that is intended, by at least one of its participants, to disrupt" business, transportation, schools, government, or free assembly." Keep in mind, that means if you start a food fight, you could be a terrorist under this law.
To say nothing of the thousands of anti-war protesters who have been arrested over the past few months.
Or union members who go out on strike.
"Emergencies" have always been tyrants' favorite excuse for setting aside constitutions.
> I remember when Cyrix had it's 100MHz CPUs with huge fans and everybody tweaked them to 133MHz, every long-term calculation on that involving FPU would give random numbers as the result...
Bah, the early Pentiums would do it without the need for overclocking.
Slashdot Mirror
> I guess comparing spaceship sizes is really important to
Maybe they don't realize that sometimes a starship is just a starship.
>
In Greek, yes. But in English it's usually just "lemmas".
Unless you're like me (and lots of other geeks) and like to use exotic word forms for the fun of it. My dictionary gives both forms, but you're probably the first person (other than myself) whom I've ever heard using the -ta form.
> but the biggest problem (as I see it) is that there is lots and lots of code which does not really lend itself to easy proof (e.g. timing-dependant networking code, GUI code, parallel/distributed code, etc.).
I've never seen proof work for GUIs, but there are methods for doing proofs for time-dependent and/or distributed programs.
> You don't have to provide formal proofs of all code. I would estimate 90% of all array accesses could be done without any run-time checking if...
I'm not so sure run-time checking is such a bad thing. Sure it adds a bit over overhead, but we have a very wrong fixation on performance over correctness. IMO correctness should always be more important than performance. If your boss puts more emphasis on speed than on correctness, just turn in a "Hello World!" program for every project: programs don't get much faster, and BFD if the output wasn't what your boss wanted -- it's just a bug!
Besides, in most cases run-time checking is going to impact performance far less than the inefficient algorithms people tend to use. I shudder at some of the programs I've had to repair because the people who wrote them didn't know the advantages of the most rudimentary data structures, such as trees, in many common circumstances.
> I've rarely had to "work against" strong type systems in the past. Sufficiently expressive type systems are important for this to make sense, I'll admit that; it requires a certain kind of thinking to be able to make use of strong typing effectively. This restriction on "free thought" may be what people find most offensive, but I'm not sure.
That is also my experience, and my perception of why people don't like it.
Strong typing does seem like "a lot of extra keystrokes" and a lot of extra chains on your behavior when you first start using it (no, I'm talking about strong typing, not what passes for that in C++). But after you get used to it you find yourself creating very sophisticated abstract data types and thinking of them as abstractions, so that the programming end becomes very simple and elegant -- as well as completely eliminating certain kinds of bugs that programmers waste an incredible amount of time fighting.
I try to get people to think of strong static typing as a form of constraint-based programming. All a strong type definition actually does is put some constraints on the values a variable or parameter can have. And it's a nifty kind of constraint, because you specify it once rather than all through your code, and because it can be checked at compile time rather than at run time.
> But, at the same time, I truly hope that mechanisms for proving properties about programs will become not only more powerful, but also more widespread.
I also am a fan of formal verification. Unfortunately, formal verification requires a formal specification (to be prove to have been implemented correctly), and once you get to complex application programs (rather than, say, just a sorting routine), providing a correct formal specifications is probably going to approximately as difficult as writing correct programs is now. IOW, it just moves the problem somewhere else.
> > They are less efficient, just as BASIC or C is less efficient than pure assembler,
> They are _NOT_ less efficient. Depending, of course, on your definition of 'efficient': CPU-efficient or Programmer-time-efficient?
I hear that even in terms of CPU-efficiency, some optimizers produce code that runs faster than what humans would write in assembly language in practice.
He's simply wrong on this one. A list is a data structure, so strings are only a special kind of list if you choose to implement them that way.
In terms of pure abstraction, both strings and list can be thought of as "finite sequences". But strings and lists are not used the same way by programmers (or other people), so there's absolutely no reason to presuppose that they should both be implemented the same way.
In fact I would go further (away from him) and say that the common paradigm of treating strings as arrays of characters is poor design as well. Arrays probably are the best way to implement strings, but from the language design POV they should IMO be treated as a distinctive data type of their own, with native support for the most natural operations and whatever underlying interface works best.
Notice that I say that as a fan of s-expressions. Some of us draw a line between "fan" and "fanatic".
> Why is it, if a Leftist politcal agenda is advanced in a work of "art", the creators are credited with depth, greatness, and strength of character, and yet when a Rightist political agenda is advanced, the creators are jingoist, reactionary, and fascist?
Maybe because artists tend to be leftist, so that most rightist "art" must perforce be made by someone other than artists?
> What part of "The 3-person team from North Vancouver, Canada" did you not read? Anime, in the terms commonly used by American fanboys, refers to Japanese Animation.
This is canime?
> And he considers something like Object-Oriented Programming a slow evolution?
When you consider that it is just a metaphor for refinements of pre-existing ideas such as data hiding, which in turn are refinements of pre-existing ideas such as structured programming, which in turn are refinements of pre-existing ideas such as "high level" programming languages,
See past the hype.
> They're utterly deserving of whatever graphic Slashdot brings to the site.
You refer, I suppose, to a graphic slashdotting?
> When you are building any formal system you have to start with a set of Axioms. If you throw out the Axiom "people think" what do you have to go on? In essence by throwing out the axiom, you are setting up a situation where anything could be considered thinking, because there is no foundation to compare it with.
Science isn't a formal system; it doesn't have axioms. We have to do as best we can simply by looking to see what happens and then trying to understand it.
So we have this notion that "people think", and we have a very vague notion of what "think" means. Where do we go from there? If we start with the notion that thought is something special that can't arise from mechanical processes, we've answered our question by fiat.
But some of us would like to understand how thinking works rather than having an ex cathedra pronouncement that sets it outside of science from the get go. And everything we've learned about the body, the brain, neurons, neurotransmitters, indicates that humans are just big complex machines with no special ingredients. And in the past few centuries we've made marvelous progress at understanding how these components work, with never a need to invoke the supernatural, metaphysical, etc., yet.
So our question for Searle and his ilk is, what the heck is this human "understanding" if not the result of mechanical processes? If it's not the result of mechanical processes, we'd like to see some evidence for that. If it is the result of mechanical processes, why can't it be done in a computer instead of a bag of dirty water?
Searle's argument is just slight of hand to obscure the basic issues, and buying in to his argument requires accepting an 'axiom' that has no empirical support whatsoever, namely that "understanding" is something special that lies outside the mechanical operation of rules. Essentially he assumes his desired conclusion; everything else is just leaves raked over the path to hide its circularity.
No one expects the Republican Guard.
> I guess my point is, at what point should we be content to resign ourselves to letting people die, to allow them a higher quality of life?
After you, my friend!
> I don't need that. My second-hand vending machine is sitting there between my theater-style popcorn popper and the second-hand soda fountain I made after reading about it on Slashdot yesterday.
> I have all the major food groups -- sugar, salt, fat, and cholesterol -- all within reach of my computer!
Stop, stop! You're making me hungry! Now I want to run see a movie so I can get some of that popcorn dripping with fake butter.
> Wow. Technology is grand. I'll hit that 350-lb mark yet!
Next year's model will have a Snickers dispenser mounted on the side.
> Someone noticed this and placed a bet for the same numbers for the first game of day 3, and won the jackpot. As it turns out, the programmer had reset the "FOR day IN
Were "someone" and "the programmer" by chance the same person?
> It's hard to take this lawsuit seriously looking at this. And with terms like "Avatar of Techno-Wootz(TM) Damascus steel".
Woot!(TM)
> Back in my SCA days, one local sword maker described how he did it. He started with blanks intended for use as auto leaf springs. After suitable grinding, he had them heat treated. This was Cleveland when it had steel mills. He went to a heat treating shop, handed over the sword blade, said "ASTM Process 50, 4 hours". They said "It'll be ready Thursday".
You mean, all those years I spent quenching my swords in the flowing blood of one-eyed transvestite lumberjacks of royal ancestry, and I would have done just as well taking them down to Edgar's Cut-Rate Annealing in batches of fifty?
> Or, consider the fact that Senate Bill 742 in Oregon, introduced by Republican John Minnis, would define as a terrorist, a person who "plans or participates in an act that is intended, by at least one of its participants, to disrupt" business, transportation, schools, government, or free assembly." Keep in mind, that means if you start a food fight, you could be a terrorist under this law.
To say nothing of the thousands of anti-war protesters who have been arrested over the past few months.
Or union members who go out on strike.
"Emergencies" have always been tyrants' favorite excuse for setting aside constitutions.
> But they don't control what you read.
If they scare you away from reading it they do.
> Utimately, they want to replace our democracy with a plutocratic theocracy under their brand of Christianity.
What don't they like about the one they have now?
> ush already believes that he was elected by God to lead this country.
Wow, I didn't know God was on the Supreme Court!
> They will have bioluminescent backlit displays and be powered by human farts. And yes, there will be a headphone jack.
Just be careful not to plug the headphones into the auxiliary power outlet, or you may not like what you hear!
> I remember when Cyrix had it's 100MHz CPUs with huge fans and everybody tweaked them to 133MHz, every long-term calculation on that involving FPU would give random numbers as the result...
Bah, the early Pentiums would do it without the need for overclocking.
> That could buy a really large Beowulf Cluster
of lawyers.