If anything I think the discussion demonstrated the point that we still don't know how to write safe programs with any degree of certainty, and that any program is as good as the programmers who produced it. So for me the term "Type Safety" is a bit of an oxymoron, because being type safe doesn't infer program 'safety' at all!
Accepting that there is no guarantees, perhaps we should let go of the pink past and explore the new blue OO idea a bit further. To do this we need to take a pure OO approach, with scant regard for incumbent technology. Croquet is a project that chooses to look at software Engineering afresh from a pure OO perspective. The question posed by Croquet is:
If we were to start again, and build an Operating System with modern assumptions about computer power, what could we do today?
To this question the Croquet team have come up with some answers:
- A VM that works bit identical on all platforms. They achieve this by writing the Squeak Smalltalk VM in a subset of Smalltalk itself, called Slang.
- Given bit identical behaviour, replicate objects across the web, with the guarantee that replicated objects will behave bit identically.
- Using Object Replication, and synchronised message sends, create a shared virtual Time and Space, across the web, they call this TeaTime.
- Use Peer-to-Peer communications to remove the bottle neck of centralised servers.
- Late-binding to ensure that the system can grow and change organically. Also allow non Croquet components to be consumed into the Croquet world.
I will explore Croquet in detail over the next few blogs. Here is an article which is a excellent primer on Croquet for the uninitiated. It is difficult describing Croquet, because like the Sony Walkman, Croquet is something new and innovative, and unlike anything we have seen before. The closest description to the vision held out by Croquet is the virtual computer world presented in the movie "The Matrix".
Croquet is The Matrix.
51 comments:
I am a bit puzzled by the start of your post, as it seems to contradict the conclusions we came to at the end of your last one, which was that far from being an oxymoron, it was clearly demonstrated that Type Safety can be a useful tool in helping towards program safety. One can hardly blame people for getting 'bogged down' about Type Safety and Program Correctness when that was the topic of your post!
Also, your statement that there are no guarantees is wrong. There have long been languages and approaches that do guarantee program safety. I have a friend who has worked in aeronautics, and all their code is guaranteed safe. Some languages like Ada were designed from the start to allow such guarantees.
So, I am afraid your justification for letting go of the past (that there are no guarantees) is mistaken.
Hi Steve,
Not wanting to get bogged down again, I think we agreed that manifest types as implemented in Java can assist in detecting bugs at compile time that could otherwise be missed at runtime.
This is not the same as saying that type safety infers program correctness.
Isaac and I have discussed the subject of program correctness further, and program correctness and type safety are largely orthogonal concerns. Take a look at the discussion after you left.
As far as I can tell, there are three sperate concerns: Program Type Safety (static typing), language Type Safety (dynamic typing), and Program Correctness (no bugs).
Program Type Safety can detect some bugs early at compile time, but it does not infer that your program is bug free (Program Correctness).
>Isaac and I have discussed the
>subject of program correctness >further, and program correctness and
>type safety are largely orthogonal >concerns.
Well, I can guarantee that they aren't, because, as I said, there are many areas in safe computing (such as aeronautic software) where type safety is used a part of the proof of correctness. You should look up the research done on the Ada language about this. The situation is that type safety alone is not enough to guarantee correctness, but in certain languages it is part of a formal mathematical system that can be a guarantee. Any statement that type safety is orthogonal to program correctness is wrong. The fact that type safety is insufficient is not the same as saying it is orthogonal.
And my other point still stands - there are certainly areas where correctness can be assured, so using that as a reason for going off into 'Blue-land' is not right. You have to have other reasons.
Hi Steve,
I know all about Ada, and it is not Type Safe. They introduced a load of non-type safe functions so that Ada was practical (coercions, conversions, casts etc).
Testing does not infer program correctness either. My point which is really a simple one is that there is no tool available that guarantees the correctness of an imperative program.
Even with functional languages where there are mathematical tools that can be used to guarantee program correctness, this still offers no guarantee. For example, it still comes down to a human being to do the maths.
Let me state it another way, even Ada, without the Non type safe extensions, all you can do is prove that your program is self consistent, and it could be self consistently wrong!
Like I say in my blog we haven't invented a way to guarantee program correctness, and in the final analysis it still comes down to programmers.
Hi Steve,
I am not offering the "Blue" plane as a solution for program correctness. I am just pointing out that colloquially, the idea of greater 'safety' is perceived as a reason to stay in the pink plane. I am suggesting that we aren't safe in either the pink or blue planes, and the idea that 'safety' is a consequence of manifest typing as implemented in languages like Java has been overstated IMO.
I have conceded your point with regards to concrete implementations of implicit interfaces and dynamic (duck) typing. But this is a relatively narrow point with respect to any guarantee of program correctness.
My reason for discussing the blue plane is to explore the possibilities that open up once we overcome what to me appears to be a largely irrational fear.
All Engineering is about trade-offs, and to make intelligent choices we need to explore all our options in the round. This is where I am going.
I also know about Ada, as I studied at York University, where much of the work was done on it. I had some of the people who worked on Ada as my tutors.
"I know all about Ada, and it is not Type Safe. They introduced a load of non-type safe functions so that Ada was practical (coercions, conversions, casts etc)."
Yes, which is why safe subsets of Ada (such as SPARK or Safe Ada) are used when safety needs to be guaranteed, so you can't use this reason.
There really are tools that guarantee the correctness of a program (whether it precisely meets the specifications provided by engineers) and we have definitely invented ways to guarantee program correctness - as I said, I have a friend who works with these tools all the time, and you use the results of such tools whenever you fly!
You simply can't get around the fact that can type safety can take you part of the way to proof of correctness, and to claim it is orthogonal (i.e. irrelevant) to correctness goes against decades of computer science and use of this factor in safety-critical systems.
This kind of development is rare - it involves using special compilers that can guarantee precisely which machine code instructions are generated for any given statement in the development language, but to deny it exists or is possible and that typing is not a crucial part of it is just plain wrong.
Hi Steve,
Here is an example of where over reliance on tools can lead you:
Ariane 5 Flight501The software was written in Ada. I worked in defence for a few years and in practice the Ada programs contained as many bugs as C++. They just took longer to write. Like I say safety really comes down to the programmer and testing.
"Like I say safety really comes down to the programmer and testing."
No, of course it doesn't come down to just that. You can't just hand-wave away more than 30 years of rigorous computer science and practical work, simply because you happen to like using a dynamic approach.
If you were right, then all the work of C.A.Hoare, and all the work put into analysis tools and the design of safe languages was a waste.
And, of course they aren't.
My friend works in aerospace safety-critical development right now, and I had a conversation with him last weekend in which he described how development was done. He works in a team that does formal proof of correctness. I really don't think he was lying!
You picked the wrong example with Arianne 5 - that is precisely the kind of error (a data conversion problem) that current analysis tools, used both at the source code and machine instruction level, would pick up. In fact, this error occurred precisely because not enough tooling was used - they disabled a software check in one area of code, and 'trusted the programmers'.
No Steve,
The problem was people. The conversion from one type to the other could not be detected at compile time. This could only e checked at runtime. So any dynamically typed language with runtime exception hanlding would have done here (i.e. even Smalltalk).
To add to this they assumed it would work because it worked on Ariane 4. If they had tested they would have detected the bug at runtime. The reason why they did not have a handler for the runtime exception is because they hadn't tested.
You talk of all this science. I have programmed for 17 years, and my experience tells me that people introduce bugs, and testing by people is how bugs are discovered and removed. Tools help, but it is the people that determine safety.
I am not making arm waving arguments. I am being very precise, about what static type provides and what it doesn't. On the contrary I believe you are presenting an arm waving argument based on a single scenario and ill-defined science.
Please be specifc. Give me a concrete example of this guarantee you speak of.
We just discussed type safety in my programming languages course, so I figured I'd post the prof's definition.
A language that is type safe has the following 2 properties:
Preservation
If an expression e evaluates to v and e has type T, then v has type T
Progress
If an expression e has type T then either:
- e is a value
or
- e evaluates in one step to an expression e' that also has type T
This means that it *does* infer program safety: Execution will never arrive at a point from which it cannot continue until it has computed the final result value. That's quite a strong guarantee.
If you don't have it, then, like C, you have to allow all sorts of operations that just become undefined behaviour.
( Of course, working exceptions and such in makes the type system more complicated, but the property still holds. )
Hi Mess,
It infers that the program is self consistent. It does not infer program correctness.
BTW most so called type safe languages don't even do this. The moment you allow for conversions or coercions, or casts you will not know whether your program is type safe until you run it. As I understand it your program may be type-unsafe (contains casts etc), but your language(runtime) is type safe and will throw an exception at runtime if it detects a typing error. This is what I referred to as Strongly typed without loopholes in my previous post. If you have a type safe language, then you still need to handle the exception.
So type safety is all about detecting tying errors. But this is not program correctness. Program correctness has to do with the correct operation of the program with respect to the requirements. There are several common errors that have nothing to do with types that will can lead to incorrect behaviour. A common example for Java is null pointer exceptions.
I introduced the term 'program safety' as a play on words and to contrast 'program correctness' with'type safety' and to stress the difference in meaning of the word 'safety' for program users.
The correct term is program correctness. Run this by your lecturer, and I'm sure he will agree with what I have stated here.
"So any dynamically typed language with runtime exception hanlding would have done here (i.e. even Smalltalk)."
No, sorry, that doesn't follow. Just because one kind of error
You are putting forward a very strange argument: because static type safety doesn't take you all the way to proof of correctness, throw the whole thing out and go off in a different direction.
"You talk of all this science. I have programmed for 17 years, and my experience tells me that people introduce bugs, and testing by people is how bugs are discovered and removed."
Well, one person's experience doesn't make an argument. I have been programming now for 30 years, and my experience tells me that tools and type safety can help find bugs in addition to testing. I proved that in the conversation regarding your last blog entry. I can't see why you are ignoring it now.
"I am being very precise, about what static type provides and what it doesn't."
No, you aren't. You explicitly say that static typing is "orthogonal" to program correctness. Orthogonal specifically means "has no influence on", which is nonsense.
"On the contrary I believe you are presenting an arm waving argument based on a single scenario and ill-defined science."
I just can't believe you posted this. How can you possibly call all the work on proofs of correctness done at major universities all around the world (and still a major subject for research) "ill-defined science"? That is an outrageous insult to thousands of academics and engineers.
It isn't hand-waving. It is well-established and robust science and math.
"The reason why they did not have a handler for the runtime exception is because they hadn't tested."
No, the reason they did not have a handler for the runtime exception was because the decision was left to programmers who did not follow the correctness specification, and instead attempted to time-optimise the code by hand.
"Please be specifc. Give me a concrete example of this guarantee you speak of."
OK. Many flight control systems in fly-by-wire planes have to be proven correct to the nearest machine code instruction. The specification is worked out precisely, coded precisely in (say) Safe Ada, that source code is statically checked, with all possible paths through the code analysed. It is then compiled to machine code. That machine code is checked against the predicted machine code expected from the compiler. Then, that machine code is statically analysed against the specification, and then it is dynamically checked, with all the state transitions of every instruction predicted (which is why this can't be done on processors with microcode), and those checked against the specificiation. All of the possible state transtitions of the machine code are linked mathematically back to the original specification, so it is possible to prove that the machine code does exactly what the specification says.
Static Typing is a critical part of the static analysis stage, and a critical part of defining precisely each machine code instruction. The analyses would not be possible without it.
Yes, this does require human input, and it does require dynamic testing in addition to static analysis, but to claim that type safety has no relevance or that one should cut back on tools is just rubbish.
Go off in your 'Blue direction' if you want to - perhaps because it is fun or productive for certain kinds of uses, but to try and justify doing that by rubishing type safety as something irrelevant to matters of correctness is to throw away decades of research by people who know far more about this than you and I.
And...
"So type safety is all about detecting tying errors. But this is not program correctness."
Go tell that to the Ada designers. It is a critical part of many procedures for proving program correctness.
I missed something off my first paragraph:
No, sorry, that doesn't follow. Just because one kind of error can't be checked by static analysis, it does not follow that static analysis can't check most others.
Hi Steve,
Just because one kind of error can't be checked by static analysis, it does not follow that static analysis can't check most others.
Agreed. But in reality it is the other way round. Static typing can only detect very few typing errors that would not otherwise be detected by dynamic typing (Strong typing). And typing errors in general (both static and dynamically checked) are only a small subset of all the programing errors possible.
Like I say, provide your concrete example of how static typing guarantees program correctness. It doesn't.
This is the type of confusion I mean. Hopefully we can clear this up so that we can move on to Croquet.
"Like I say, provide your concrete example of how static typing guarantees program correctness. It doesn't."
That is not what I am saying. I am saying two things:
(1) If you want to use formal methods for proving program correctness, then static typing is a key part of that.
(2) Static Typing can help towards program correctness.
Never have I said that Static Typing 'guarantees' program correctness. If you look at formal methods for proving correctness you will see that much more is needed in addition.
This is why I think your phrase 'Type Safety is a bit of an oxymoron, because being type safe doesn't infer program 'safety at all!' is at the best extremely misleading, and at worst simply wrong, as it can be demonstrated mathematically (which is what the research into formal proofs has shown) that type safety certainly can infer program safety to a degree, in the right circumstances.
If you are going to plunge Deep into the Blue, you need to be clear about the reasons :)
Hi Steve,
If you are going to plunge Deep into the Blue, you need to be clear about the reasons :)
I'm being very clear. Static type safety does not gurantee program correctness, so the lack of static type safety on in itself does not present a reason not to plunge into the blue.
Like I say, the benefits of static typing with respect to program correctness, have been over stated IMO. I have agreed (several times) that static typing can contribute to program safety, but so can dynamic typing, and a number of other programming practices.
Singling out static typing in this way is like saying, not drinking Whisky before programming will contribute to program correctness. It will, but it doesn't provide a guarantee :^).
You simply can't get around the fact that can type safety can take you part of the way to proof of correctness
There is no such thing as partly proven. Either it is proven or not. Try telling the Ariane 5 investors that well it partially worked! As the Ariane 5 example shows, the closest we can get to guaranteeing correctness is to test mercilessly. Can we move on now?
Hi Steve,
Then, that machine code is statically analysed against the specification
Please expand. Is this step in your proof done by a machine? If so how?
Hi Steve,
"So any dynamically typed language with runtime exception hanlding would have done here (i.e. even Smalltalk)."
This is true. For Ariane 5, if they had tested, then the code would have thrown an exception. For this specific bug any dynamically typed language would have been sufficient to detect this bug at runtime, if they had chosen to test. This is a concrete example of where static type safety did not help and the resultant error cost millions. This is what I mean by over stating the case.
Do you disagree?
"Static type safety does not gurantee program correctness, so the lack of static type safety on in itself does not present a reason not to plunge into the blue."
I don't see how you come to this conclusion - this seems a total non-sequitur to me. Lack of complete type safety certainly can be considered a reason not to plunge into a situation with no type safety at all. It may not stop you doing this, but it is certainly isn't any kind of justification.
"There is no such thing as partly proven. Either it is proven or not."
Nonsense. I have recently been reading 'Fermat's Last Theorem' by Simon Singh. Great book. The guy who solved the theorem spent years working on a proof. But the proof was only partly correct. According to your approach, he might as well have abandoned everything, and thrown all his work away. Of course, he didn't. Being partly correct about the entire Theorem involved being fully correct about almost all of it, and that was useful in itself. He then went on, and fixed the problem, based on the bits that he knew were right.
What matters is how close we get to proof (at least in programs that can't be proven formally). Using things that get you as close as possible is better than abandoning the idea, and I as proved to you in our last discussion, Static Typing can help.
It is the seatbelt issue again, Paul. Would you abandon wearing a seatbelt because "there is no such thing as partial safety - either a car is safe or it is not"? I don't think so.
"As the Ariane 5 example shows, the closest we can get to guaranteeing correctness is to test mercilessly. Can we move on now?"
I think you need to look at the example again. What the example showed was what happens when programmers are arrogant and assume that they know more than the facilities provided by tools and by the language!
Well, we can abandon this discussion if you like. But I have little interest in a discussion of a technology (Croquet) if that discussion is based on what I believe to be false premises. But if you aren't interested in my views, that is fine - I'll shut up :)
As for your other comment:
"Please expand. Is this step in your proof done by a machine? If so how?"
I don't actually know. I know that the specification is translated into a precise mathematical representation, and the state changes resulting from the machine code are compared against that representation. I would assume that there are tools to do this.
"This is true. For Ariane 5, if they had tested, then the code would have thrown an exception. For this specific bug any dynamically typed language would have been sufficient to detect this bug at runtime, if they had chosen to test. This is a concrete example of where static type safety did not help and the resultant error cost millions. This is what I mean by over stating the case.
I certainly do. This is the kind of error I was talking about in our last conversation. They didn't test because they didn't realise they had to test (a bit like that Currency matter, and the views of your colleagues).
What you are ignoring is that much of the rest of the code was proven correct, with static typing as part of that proof. Abandoning typing altogether would have been just plain nuts, as is any idea you could write safety-critical programs in dynamic languages like Smalltalk.
steve wrote I am a bit puzzled by the start of your post, as it seems to contradict the conclusions we came to at the end of your last one, which was that far from being an oxymoron, it was clearly demonstrated that Type Safety can be a useful tool in helping towards program safety.
Steve I agree, in no sense has Paul shown that type safety is an oxymoron.
However, I think it's possible that you mean something different by type safety than The property stating that programs do not cause untrapped errors.
paul wrote in the blog entry So for me the term "Type Safety" is a bit of an oxymoron, because being type safe doesn't infer program 'safety' at all!
I suppose it is possible that you don't actually know what oxymoron means - a figure of speech in which apparently contradictory terms appear in conjunction.
"dangerous safety" is an oxymoron.
"type safety" is not an oxyoron.
Hi Isaac,
True, what would a better term be?
Hi Steve,
There is no false premise with regards to croquet and type safety. Croquet is partially type safe. Just like Java. I was merely concludng the discussion on type safety, and saying that the benefits of static type safety IMO are overstated.
This is just my opinion. I am not trying to convince you otherwise, but your argument that static type safety is part way to proof of program correctness just doesn't hold water IMO. In the same way that dynamic type safety is not part way to a proof of program correctness either.
I have given a concrete, well documented example of a program error that cost millions despite static types. Part of the reason I'm sure that the Ariane 5 team did not test, was because of a niave belief that the programming language was going to protect them. It didn't.
I understand your seat belt analogy, but I do not want to rely on a seat belt that may work some of the time. I want something more reliable then that, and for me that is unit tests.
Like I say I am not trying to convince you, and this has nothing to do with Croquet.
Hi Steve,
I certainly do. This is the kind of error I was talking about in our last conversation. They didn't test because they didn't realise they had to test (a bit like that Currency matter, and the views of your colleagues).
This is where we fundamentally disagree. They didn't test because they didn't choose to test. The code worked on Ariane 4, so they assumed it would work on Ariane 5. Dispite the fact that Ariane 5 used different hardware. This is what I mean by overstating a case. No way would a static type check be able to detect subtle differences in hardware - yet they were lulled into a false sense of security that cost millions. The report on the failure partially blamed management practices - which is my point, it always comes down to people.
Steve,
Back to the currency issue. IMO this was poorly stated design requirements. It was unclear to the programmer that monetary values should be represented using a specific class. It is true that static typing wuld have helped here, as any exisitng code would have use the right type (hopefully), but so would an explicit test.
Incidently relying on exisitng code is not a good idea. I have seen code that was wrong or badly designed used as a template by others that come along later, thus propogating flaws in the code. What the code should do should be clearly understood and specified incase the exisiting code is wrong!
The reason why a programmer would not test against the design requirement for Currency, is because it wasn't specified and he didn't know. This is why your proof argument is flawed. Some one needs to talk to the customer and interpret requirements, and create a design. The logic in this interpretation may have gaps, or be flawed. You cannot perform a static check against verbal requirements. So the weak link in all of this is the human brain. Your type checker is not intelligent so is not a substitute.
I worked in a company that was commited to Ada, but over time switched to C++, because in the end the language did not provide any significant benefit. What they did instead, was to spend more time on QA with the time saved from not having to write over verbose Ada code. In the end this improved code quality and reduced bugs.
I am not making an academic argument, I am talking from real world experience.
Hi Steve,
This is the conclusion of the report on the Ariane 5 disaster:
This loss of information was due to specification and design errors in the software of the inertial reference system.
The extensive reviews and tests carried out during the Ariane 5 Development Programme did not include adequate analysis and testing of the inertial reference system or of the complete flight control system, which could have detected the potential failure.
The use the same words I have been using. Type safety cannot eliminate human error.
paul wrote in comments True, what would a better term be?
Tautology.
Stating that wearing a seatbelt doesn't imply that we won't be in an accident is true but redundant.
Stating that type safety doesn't imply program correctness is true but redundant.
(Where type safety means The property stating that programs do not cause untrapped errors.)
It would be much better to talk about one of the techniques used to implement type safety - static type checking.
Steve's argument is that static type checking demonstrates the absence of a particular category of program error - and thereby contributes to demonstrations of program correctness.
Hi Isaac,
Steve's argument is that static type checking demonstrates the absence of a particular category of program error - and thereby contributes to demonstrations of program correctness.
I agree that static type checks can eliminate a certain category of error, but that still leaves the majority of potential errors undetected (all runtime exceptions for example).I have spoken about static type checking and it's limits. I have given examples such as the Ariane 5 example. I have stated my preference for tests irrespective of the use of static type checking or not.
To me it is quite clear. What is your take?
me22 wrote I figured I'd post the prof's definition ...
Seems to be the same as the definition of type soundness p261 Programming Languages: Application and Interpretation
"They didn't test because they didn't choose to test."
There little difference between didn't choose and didn't know - both illustrate the problem about reliance on developers.
"No way would a static type check be able to detect subtle differences in hardware - yet they were lulled into a false sense of security that cost millions."
Actually, a static type check certainly could detect 'subtle' differences in hardware (like the difference between 64-bit and 16-bit).
"The reason why a programmer would not test against the design requirement for Currency, is because it wasn't specified and he didn't know."
No, this is rubbish. The programmer did not test against the design requirement for Currency not because it wasn't specified, but because the programmer was not qualified to work in this area. In the area of finance, the requirement for Currency is patently obvious. Would someone have to specify the use of an 'int' for a loop?
"This is why your proof argument is flawed. Some one needs to talk to the customer and interpret requirements, and create a design. The logic in this interpretation may have gaps, or be flawed. You cannot perform a static check against verbal requirements."
This is total nonsense, and I can't believe I am reading such a defence of incompetence! For anyone who has anything to do with financial software, the use of Currency types is essential. I have provided you with links to show this. You no more need to discuss this in terms of design than you need to talk about not using cardboard to build cars! It is ludicrous to talk of anyone having to 'talk about customer requirements' to deal with currency correctly. There certainly is a static request available for verbal requirements. The customer says "This is a program that deals with currency", and the test is to use BigDecimal.
"I am not making an academic argument, I am talking from real world experience."
You think that is some kind of positive argument?
This is yet another slur against academics. Sooner or later you will realise that academic work in this area is founded on vastly more real world experience than you have, and perhaps then you will learn a little humility and realise that thousands of people have studied this area and know far more about this than you (or I!).
I have lost patience with this, as you seem to be learning nothing from these discussions.
Isaac has given me things to look up, which is useful, but other than that, I see no merit in continuing this debate. All the answers to your questions are easily accessible.
And as Isaac says, I really don't think you understand what 'oxymoron' means....
Hi Steve,
... You claim that what I have said about requirements analysis, design specification and types is nonsense. Like I said I'm not trying to convince you. As for academics, no slur was intended.
... What about the rest of my post? Did you read the article on Croquet? What do you think?
Hi Isaac,
I've looked up tautology, and I see where you are coming from and it is close, but it doesn't quite express what I mean either.
My difficulty with the term type safety is the use of the word safety. The word has a conitation that infers freedom from fear.
Fear is a strong motivator. And talk of type safety is often associated with programmers fears. A lack of program correctness is a primary fear for most programmers, and colloquially type safety is seen as a technique that at least in part addresses this fear. I just think Type Safety is an unfortunate term. 'Type checked', is better because it indicates that a certain type of error is being checked for, but does not imply that the program is safe in anyway.
It is interesting the emotion the word safety can trigger. In an academic sense type safety doesn't mean much (using your defintion, or the one on the c2 wiki). But colloquially type safety evidently means a lot more then either of our definitions state. At least Steve, and Mess seem to think so.
paul wrote in comments My difficulty with the term type safety...
It seems like your difficulty with the term type safety is the same as your difficulty with the word oxymoron - you don't actually understand (or prefer not to understand) what it means.
paul wrote in comments My difficulty with the term type safety is the use of the word safety. The word has a conitation that ...
Seems like you have taken the word "safety" out of context, ignored it's primary and secondary meanings, and fixated on a single connotation - how incredibly bizarre.
paul wrote in comments There are several common errors that have nothing to do with types that will can lead to incorrect behaviour. A common example for Java is null pointer exceptions.
You are mistaken.
Not only is a NullPointerException an example of a type error, it's a programming error that in many cases can be detected by static type checking in other languages.
Hi Isaac,
Not only is a NullPointerException an example of a type error, it's a programming error that in many cases can be detected by static type checking in other languages.
If Java's null was a true object like Nil in Smalltalk then true null pointer could be avoided by using the type system. Strongtalk does this.
What I am talking about is runtime exceptions like the one that took out Ariane 5. Now your views on the difference beween type safety and program correctness have been recorded on this blog.:
Type safety does not decrease the risk that something might go wrong - type safety decreases the risk of bad stuff happening when something does go wrong.
and
type safety is about what happens when your program has a particular kind of error, not about whether it has a particular kind of error.
afaict what you mean by program safety is no different from what everyone else calls program correctness, and it has nothing to do with type safety.
Have you changed your mind? Or is this just blatant opportunism?
What do you think about Croquet BTW?
Hi Isaac,
... As for my dislike of the term Type Safety, you only have to look at this blog to see why it is a poor term. There are as many opinions of what it means as people. Your definition:
A programs that does not cause untrapped errors.
Is ambiguous. I will assume that you mean untrapped type errors, otherwise like I've pointed out already your definition doesn't make sense.
Steve seems to think that you can express user requirements using mathematics, and some how type safety addresses requirement analysis errors. I won't comment on this view.
The best definition I've come across is the one on the C2 wiki:
Any declared variable will always reference an object of either that type or a subtype of that type.
But they quickly go on to break this definition down into lesser partial forms, because they accept that in practice full type safe languages do not exist.
I think this discussion about Type Safety speaks volumes, and makes my point.
paul wrote in comments There are several common errors that have nothing to do with types that will can lead to incorrect behaviour. A common example for Java is null pointer exceptions.
paul wrote in comments If Java's null was a true object like Nil in Smalltalk then true null pointer could be avoided by using the type system.
So you agree that your comment that NullPointerException has nothing to do with types is completely wrong?
paul wrote in comments Now your views on the difference beween type safety and program correctness ... Have you changed your mind? Or is this just blatant opportunism?
I guess you think there's some kind of contradiction between those quotes and something else. What is this contradiction you imagine - you haven't actually told us?
So you agree that your comment that NullPointerException has nothing to do with types is completely wrong?
I can see this debate has served it's usefulness :^) For Java NullPointerException is a runtime exception, which by definition can only be detected at runtime, and cannot be detected by a static type check. Null has no type in Java and is not a variable in Java. It stands in for an undefined variable.
I'm sure you know this. Or maybe you don't?
Hi Isaac,
So you stand by your original views on type safety and program correctness. That is good to hear, because I actually think you are right here.
To be honest I'm tired of this, and I have satisifed myself about Type Safety and it's usefulness. How about writing a blog post of your own on type safety if you so desire? I would rather talk about Croquet.
paul wrote in comments Null has no type in Java ...
You are mistaken.
"There is also a special null type, the type of the expression null, ... The null reference is the only possible value of an expression of null type." Java Language Specification
paul wrote in comments Null has no type in Java and is not a variable in Java.
Please show where I said null was a variable.
paul wrote in comments dislike of the term Type Safety ... Your definition: A programs that does not cause untrapped errors.
Please show where I used that definition of type safety - I have consistently referred to Krishnamurthi's definition and Cardelli's definition.
paul wrote in comments I will assume that you mean untrapped type errors, otherwise like I've pointed out already your definition doesn't make sense.
You've already seen a definition for untrapped error, please show where you pointed out that definition doesn't make sense.
paul wrote in comments To be honest I'm tired of this ... I would rather talk about Croquet.
You repeatedly put words into my mouth and misrepresent what I and others have written.
You repeatedly claim to have demonstrated something without being able to show where.
You seem to have no interest in whether what you write has some basis in reality or is blatantly wrong.
I have no reason to think that you would behave any differently if the subject was Croquet.
Paul said...
I have made no claims. I have merely stated opnions. Incidently it is still unclear to me what exactly about what I've said you disagree with.
.. You have said that the word oxymorom is inappropriate and I agreed.
..You have said that type safety and program correctness are orthogonal concerns, and I have agreed with this too.
... You have given several definitions of type safety, which once we cleared up the ambguity I agree with also.
...You now want to argue with me over whether NullPointerException is a rumtime exception or a type miss-match.
Frankly I don't care. My point is that it occurs at runtime and can not be detected by a static type check.
It is clear to me that all you want to do is argue. Well I'm tired so please go argue with someone else!
paul previously wrote in comments My goal is to communicate and exchange ideas.
paul wrote in comments It is clear to me that all you want to do is argue.
argue: exchange view or opinions
Oxford English Dictionary
paul wrote in comments My point is that it occurs at runtime and can not be detected by a static type check.
class nulltest {
public static void main(String[] args)
{
String s = null;
System.out.println(s.length());
}}
Exception in thread "main" java.lang.NullPointerException at nulltest.main(nulltest.java:4)
#1
void main(String[] args){
String s = null;
println(s.length());
}
line 2, column 11:
The value null cannot be assigned to s because it might be null.
#2
void main(String[] args){
?String s = null;
println(s.length());
}
line 3, column 14:
No possible call for length.
Arguments: (?java.lang.String)
#3
void main(String[] args){
?String s = null;
if (s != null) println(s.length());
}
nulltest: parsing
nulltest: typechecking
nulltest: generating code
nulltest: linking
nulltest: writing in archive
>java -jar nulltest.jar
>
#4
void main(String[] args){
?String s = "a String";
if (s != null) println(s.length());
}
nulltest: parsing
nulltest: typechecking
nulltest: generating code
nulltest: linking
nulltest: writing in archive
>java -jar nulltest.jar
8
>
As I said "... it's a programming error that in many cases can be detected by static type checking in other languages."
Hi Isaac,
You are pathetic. I spoke about Java. I agreed about other languages
It is in the record. Here for everyone to see. Please just go away!
Isaac said:
You repeatedly put words into my mouth and misrepresent what I and others have written.
You repeatedly claim to have demonstrated something without being able to show where.
You seem to have no interest in whether what you write has some basis in reality or is blatantly wrong.
The irony is that everyone of these actions you attribute to me exactly describe your behaviour.
I have read about your attack on Craig Larman, and even though I had read his book and found it a great piece of work, I kept an open mind. Now I know! I would rather trust anything Craig Larman had to say then to acredit any credbility to a loony nut like you.
Make your protest elsewhere. I can't help you.
paul wrote in comments I would rather trust anything Craig Larman had to say then to acredit any credbility to a loony nut like you.
Here's what Craig Larman had to say:
"My view is that sotfware engineering shouldn't be religion and should indeed be based on evidence and statistics, and I appreciate Isaac's or anybody's improvements to whatever I wrote. (I hope Isaac may be a reviewer on my next book, because he seems thoughtful)."
Hi Isaac,
There you go. Go review books. At your better moments I have found some of your comments thoughtful too. (Like the word tautology). At other times I believe that you choose not to address the issues, but to persue meaningless arguments using a dialetic style which serves no purpose (like your insistence to misrepresent what I have clearly stated about NullPointerExceptions in Java, and runtime exceptions in general).
On balance, I think this debate has long past it's usefulness. Thanxs for the debate, but I see no value in persuing it further. Goodbye and good luck!
Post a Comment