Lambda the Ultimate

I don't know enough to know if one can poke holes in your comments; they make a lot of sense to me and are appreciated. It always helps me tremendously to see such categorizations.

First, this is an excellent taxonomy that I will refer to from now on—too bad I've never seen its like in any of the literature.

But Dave Griffith has responded exactly correctly, IMHO, and said what I should have: the claim isn't that Java, Python, or Perl aren't type-safe by any definition of that term, but rather that the property that they have that Garfinkel called "type-safety" was rather "memory-safety." From that point of view, the observations following in the article make much more sense: memory-safety is indeed only one, relatively trivial, aspect of safety. But a naïve reader will likely come away with the perception that type-safety doesn't help avoid a wide class of bugs—in this case, a wider class than memory-safety alone can provide.

Interestingly, the example given of what "type-safety" can't do, ensuring that a lock is used correctly, is exactly one of the things that linear type systems do. So I'm afraid it's another case of conflating what popular type systems don't do with what static type systems can't do. If people who write about the topic would just quit making this particular class of errors, you'd find me writing a lot less on the subject.

In any case, that wasn't what interested me about the article most. What interested me most was that Garfinkel bothered to look at big, complex systems with big, comprehensive testing regimes and observe that there are still really unfortunate gaps with them, and he pointed to Lightweight Formal Methods as an alternative. I find that fascinating even leaving aside the confusion over type-safety vs. memory-safety.

...although I suspect that the taxonomy could be tightened up a bit (the issue of "unsafe" constructs ala C# or Modula 3 is really orthogonal to some of the other issues) and better formalized. Better, more appropriate labels might be invented--mine were rather ad-hoc.

Hmm... maybe someone should publish this (once done). As I currently reside in industry and not academia; I've no particular pressure to do so.

A couple of other interesting points which might be worth addressing, should someone want to take this further:

* The effect of substitutabilty, especially in type systems with subtyping. OO languages, for instance, by allowing non-Liskov subtyping, arguably permit more errors to be introduced into a program which passes the typechecker or inferencer. OTOH, proponents of OO claim (and I agree with them) that the ability to have different types which have some similarity (represented by a supertype) but observable differences otherwise, is a good thing.

* Type coercions. Many languages allow implicit type coercions which can allow incorrect programs (i.e. ones that don't do as intended) to pass the typechecker, often with bizarre results. Multiplication of strings is a longstanding example.

Not even mentioning OutOfMemoryError, there are also issues with Java memory model leading to concurrent bugs, and lately I've stumbled upon problems with permanent generation space while extensively generating classes on the fly.

Do we need another taxonomy for memory-safety? Or rather a branch on the existing one for type-safety?

can prevent out of memory bugs. (Actually, I can think of many ways that languages can guarantee their absence; it's just that those ways will make the language difficult to use and/or unsuitable for most applications).

Likewise, I'm not sure that I'd classify concurrency failures as type system bugs--the Java type system says very little about concurrency (other than that reads/writes to certain things are required to be atomic). One can, of course, treat any interesting program invariant as a type, but making practical use of such capability is still the stuff of research.

Also, I was under the impression that many of the issues dealt with in the paper had been resolved in more recent versions of Java. In particular, wasn't double-checked locking; long known to be broken, fixed in Java 1.4--the paper you cite is quite a few years old, and recent changes to the Java spec have been made to deal with these issues.

Of course, I'm of the opinion that unrestrained shared-state concurrency is asking for trouble in the first place--and that the fatal flaw of Java in this regard is its embrace of shared-state concurrency; something which won't be fixed by tweaking either the type system or the JVM. (Perhaps introduction of domains, or some other way of segregating objects into "referenced by multiple threads" and "referenced by a single thrad", might be a start).

I'm going to try to phrase this carefully.

MLKit is a region inferring ML compiler. It can statically prove the memory bounds of code. It does not make the language any harder to use than plain ML, since it's just plain ML. The question of ease of ML vs Java is open, obviously. I believe they tote it as being great for the embedded space. It actually still uses a GC, but for a much reduced set; does anyone know whether it would be possible to entirely do away with it? Would it be more possible in Haskell where purity is guranteed?

Similarly, shared-state concurrency is not a bad thing. It should be used at the same time as message passing concurrency, and can be done safely. The software transaction memory work done by the Haskellers recently has shown how to compose share state operations together safely. In Haskell, this can, and is, guranteed by the type system. I would go so far as to say that right now, the problem of shared state concurrency in Haskell is solved; I'm sure I'll get picked up on that.

In short, both of the points that you raised are true, in the sense that they are not necessarily failings of the type system. However, there is much that a good type system can do to help. I also wonder how the DT crowd would approach these two problems? Is there a standard method(s) available?

It's my understanding that region interference can compleatly remove the need for a garbage collector, but that the resulting system svallovs up to five times as much memory as a system with GC would.

The Metronome people at IBM have a (somewhat firm, from what I understand of the various arguments) real-time garbage collector for Java. I wonder if some combination of region inference (to narrow down the amount of memory to be collected) and such a "real-time" garbage collector might get closer to the limits and requirements of the embedded/RT space.

It actually still uses a GC, but for a much reduced set; does anyone know whether it would be possible to entirely do away with it? Would it be more possible in Haskell where purity is guranteed?

Despite purity Haskell still allows effects in the IO monad, so we still would need GC for MVars, IORefs and their friends.

As was already mentioned, you should update your papers about the JMM - JSR 133 changed it for Java 5. See the FAQ, for a quick reference on the changes.

Yes except i don't understand how divide by zero avoids being a type error in most statically typed FPLs.

By not being worth the pain caused ("you mean I've got to manually convert to non-zero-int before each division?"). It's not as if most statically typed FPLs don't have partial functions.

Wouldn't every language have absolute type safety then, depending on how much pain you can stand?

You mean "it's ok, it's just a partial function that happens to crash on that input"? :-) Yeah, but the alternative involves a different kind of pain that'd make much arithmetic unbearable. IMO it's acceptable in the presence of exceptions in a way that falling over because you tried to treat that integer as a pointer and dereference it wouldn't be. Undefined behaviour and exceptions're very different levels of safety.

Yes, I'm not objecting to the practice in it self, it's more about the classification. (And I seem to take for granted that functions raise exceptions rather than do something undefined.) I just think you shouldn't go calling something "Absolute type safety" then the only thing that differencing it from what you call "Nominal type safety with exceptions" is that the former only includes the exceptions that you personly happen to like. I would like some more formal distinction. At least for something containging the word "absolute".

EOPL says something about this (concerning division by zero specifically, IIRC). Shriram's book talks at length about the precise wording of the type soundness theorem.

(though not Java 5, due to issues with the generics implementation).

Interesting! Could you elaborate, or give a pointer?

Quite a few papers on the topic (many of them coming from the authors of a rival generics proposal--one not accepted by Sun/JVP--which doesn't have this problem, but requires much more substantial changes to the JVM in order to work. The rival generics implementation is similar to how C#/DotNet does it).

Perhaps I'm being a bit unfair to Java 5, as the issue doesn't arise unless you use introspection. However, the problem is essentially as follows:

Note that I use square brackets ([]) rather than angle brackets (<>) to delimit the arguments to generics, because the site software treats the latter as markup and I'm too lazy to type &lt; and &gt; all over the place.

* Java 5 generics use a combination of type erasure and silently-inserted downcasts. If you type Vector[Int] or Vector[String]; the resulting class is essentially the same as Vector[Object]. As far as the JVM is concerned, the classes are one and the same; the distinction between different parameterized types is made ONLY at compile-time.

* When you retrieve something from a Vector[X], Java essentially inserts a downcast in the retrieval operation which verifies that the retrieved object (remember, the underlying container as implemented has no knowledge of the type parameter) is indeed of type X. As the compiler verifies (at compile time) that only X's are inserted into a Vector[X], this downcast will usually always succeed in a well-formed program. This downcast is required by the JVM, as as far as the JVM is concerned, the type is a Vector[Object].

* If, however, you use introspection to retrieve a Vector[X] from something, it is easy to fool the compiler into thinking that a given term is of type Vector[X] when it's really Vector[Y]. Remember, the JVM/runtime CANNOT TELL THE DIFFERENCE.

* When the language is so fooled; and one attempts to retrieve an X from something which is really a Vector[Y], the inserted downcast will fail, throwing BadCastException. The exception occurs in a place where the user doesn't expect it--during the middle of an assignment operation which appears (to both human and compiler) to pass the typechecker.

I don't wish to downplay the cost of what the author refers to as "type safety", but it isn't as big as he would leave us to think.

The author of the vstr library did a study of real-world problems on RedHat Linux. He concluded that only about 40% of all serious problems could be prevented with a better language. http://www.and.org/vstr/security_problems This would be a great improvement, but it isn't near as large as most people think.

In the authors defense, if you read the second page of the article he makes it clear that there are other problems. However between buffer overflow type problems listed first, and that few people will read to the end, the impression is that buffer overflows are the only problem.

In truth buffer overflows are the easier problems to fix, and generally the easiest to spot.

I suspect that if Multics was used as an Internet server today it would have been cracked a few times. The parts of the puzzle are just too many and too complex. Though it would have much less successful attacks that the typical Unix or Windows system. OpenBSD was cracked, and they put as much effort into things and Multics did.

Henry Miller: The author of the vstr library did a study of real-world problems on RedHat Linux. He concluded that only about 40% of all serious problems could be prevented with a better language. http://www.and.org/vstr/security_problems This would be a great improvement, but it isn't near as large as most people think.

I'm confused: I can find neither the 40% nor the "better language" claim by following the provided link. In any case, one of the major arguments that we proponents of richer type systems make is precisely that there's more to safety than memory safety.

Henry Miller: I suspect that if Multics was used as an Internet server today it would have been cracked a few times. The parts of the puzzle are just too many and too complex. Though it would have much less successful attacks that the typical Unix or Windows system. OpenBSD was cracked, and they put as much effort into things and Multics did.

There's also more to security than perimeter security; see the E programming language and related links for the most in-depth coverage of the issues extant, as far as I'm aware. Also, saying "OpenBSD was cracked" is more than slightly disingenuous, given that it's had "Only one remote hole in the default install, in more than 8 years!"

The 40% claim comes from other posts (elsewhere) by the author. Reading the page you can see that it is close to that, though clearly only 1 digit is significant.

I don't want to get into the pros/cons of type safety. Smarter people than me have argued about it for years. There are some advantages, but there are also disadvantages.

"Only one remote hole in the default install, in more than 8 years!" was the exact point I was trying to make. Smart people who focus on security first, and carefully program (though I don't know if they use formal methods) still missed something.

E is very interesting, but the model can be broken, particularly if you do stupid things such as grant excess capabilities to something. There are many stupid programers out there. Worse there are many lazy programers. If E was common, then you can be sure that it would be common to see code that just gave some program all rights when it only needed a small amount because it is easier (you can write a script to give your program rights to everything, restricitng rights requires hand work)

Regarding OpenBSD, I think you might have an unrealistic standard if one remote hole in over eight years doesn't sound like an impressive accomplishment, especially for a very traditional UNIX system!

Regarding E, I think you're largely mistaken: E doesn't lend itself to writing code that takes a "just make everything available" stance, to put it mildly. In particular, "You can write a script to give your program rights to everything, restricting rights requires hand work" is exactly backwards. It takes a conscious effort to expose capabilities in E, since "only connectivity begets connectivity." The one thing you can't do (not just E, but anyone) is prevent subjects who should be allowed to communicate in the context of a system from delegating capabilities, but capabilities win because you shouldn't be able to express a security restriction that you can't enforce.

You misunderstand. I am very impressed with openBSD. However despite all their efforts they still failed once. Only once (so far), but that is still one time when if you were running openBSD you were vulnerable because of their mistake

As for E, they make it hard give excessive rights. However I know some programmers who will get tired to figuring out what rights everything needs, and just give all rights to everything because it doesn't matter. The E documentation lists some ways you can create a security hole with E. They are things that only an idiot would do, but there are plenty of idiots out there who program.

I don't understand what you're getting at when it comes to E, or in general, languages which enforce desirable properties. Any language can be subverted to some extent by a programmer who doesn't know any better, or one who is determined to do so. Perfect idiot-proofing is not a practical goal for Turing-complete languages.

A more important practical goal for developing better languages is to enable competent professionals, using proper processes, to do their job better, and make fewer mistakes.

Coming back to a point in an earlier comment:

He concluded that only about 40% of all serious problems could be prevented with a better language.

It's worth emphasizing that this improvement is purely based on focusing on one feature, string safety. A "better language" can provide all sorts of other advantages. The list of vulnerabilities that vstr might have avoided includes no analysis of which other language features might have addressed other vulnerabilities — use of E would certainly have addressed quite a few of them, for example, and use of garbage collection would have addressed others. The total percentage that would have been addressed by many "better languages" is clearly much higher than 40%, just based on a casual inspection of that list.

As for OpenBSD, that's a testament to what can be achieved with even very unsafe languages, using good people and good processes. Imagine what those same people might have achieved if they hadn't had to spend so much time doing jobs that their languages, used properly, could do for them.

Well you could for example make a VM that asks the user for permission before doing anything dangerous. Then a language targeting that VM coudln't possibly make an unsafe program. (basicaly the same idea as a capabillitys secure operativ system.)

It's easy to represent very coarse capabilities, like reading the specific file, but I estimate number of capabilities in programs that really use them to be so huge, and differences between them being so intricate, that no user could tell the difference between them, even if we invent some wonderful renderer for capabilities.

A reasonble question is - if a user cannot cope with this load, how a developer is supposed to? One of the answers would be compositionality. The developer deals with capabilities by baby steps. E.g., in OO setting, the developer can think of some object x as "the A I got from y" and about object y as "the B I got from z", etc., not as "the object with OID 1234567890". Hope my clumsy explanation is somewhat understandable :-)

Granma's Rules of POLA are supposed to provide some useful rules of thumb for the everyday user of a capability based system.

There are. The problem is whether a file is known-open (or in the example, known-closed) in a given branch or not, although typing can also be used to force the presence of run-time checks ("you can read if you've checked it's open").

example (I remember I have posted this before, but anyway):

File create() -> closed;
void open(File file -> closed) -> open;
void close(File file -> open) -> closed;

Then a compiler could easily check the flow of the code to see if the user-defined states are honoured by the code.

Program flow should be strongly typed.

You're trying to fake dependant types again. Open and closed are obvious subtypes (or parameterisations - File Open vs File Closed vs File any) of File. Then you just do the linear types thing, much as you're requiring.

...it is a nicer (methinks) way to declare those types, as well as being open to extend the types without much strange grammar. It is something the average Joe programmer will consume much more easily.

Not as-is, you've not got a fully-specced mechanism. I do like the idea of sugaring "run this linear value through a function and rebind a return value of some related type to the same identifier", but parameterising on a record or similar structure seems to be a far more appropriate way to allow the type to be extended with new properties. Otherwise you're left defining things like how individual or states relate to each other. Also, your syntax doesn't seem to handle things like multi-parm functions at all?

I have worked extensively with requirements documents provided by external companies, and I can tell you that requirements are actually types. Requirements express invariants (static/dynamic), information structure and process flow; these concepts can already be expressed with types.

If those requirements could be expressed in a formal way, then an implementation could be checked against them for correctness.

But I'm not sure how much that buys you. It still feels like this is being force-fit into a type system issue, when I don't think that it is at all.

It's true that what you can formally define (nevermind what you can intuit!) is still broader in scope than what's covered by any extant type system. This is precisely what drives type system research: we'd like to design type systems that type more programs than is currently possible, do so with a real economy of annotation, and when annotation is necessary, not have it be completely alien. So far, the progress on the first goal seems to be excellent, the progress on the second goal pretty darned good, and progress on the last goal absolutely abysmal. IMHO, of course.