Lambda the Ultimate

Just to be clear, this is just about every object-oriented language, ever. Functional languages tend to be rooted in a formal theory of functions, whereas object-oriented languages tend to be rooted in kitchen sink design. There are formal theories for OOPLs, such as the ones developed in term rewriting and coalgebraic specification.

I call BS. For example look at Featherweight Java, a core language designed for formal reasoning about programs. FJ has a formally defined type system and small step semantics. It is in fact a proper subset of Java in the sense that every FJ program is a valid Java program that, when executed on an actual JVM, yields the same result as evaluating the formal small-step semantics for FJ. There have been literally dozens upon dozens of papers that propose new features or type systems for Java that base their formal reasoning on the well-understood FJ core.

And to claim that OO languages are rooted in kitchen sink design--have you ever programmed in Self or Smalltalk?

Failing a complete formal description of small-step, big-step, or denotational semantics, most OO languages that I am familiar with define evaluation rules. If evaluation rules aren't semantics, then what, in your definition is?

Finally, the untyped lambda calculus is a formal theory, but it is usually extended with a type system to define the set of programs that are gauranteed not to "fail". This type system does not change the fact the lambda calculus is the lambda calculus; you don't need to change the basic evaluation rules to get typing.

I am not sure what you are getting at. If you took a program written in one of these typed OO languages and ignored the types and simply executed the program, it still would compute the same result. After all, the purpose of a static type system, whether for the lambda calculus or for some OO language, is to reject programs that might fail at runtime.

I wouldn't agree with your stated purpose for static type systems. I think it describes the principle of what a static type system is, rather than what its purpose is - i.e. why we use them. The counter-example makes this clear: systems are built with dynamic type systems all the time, without being rejected at compile time, and they still are able to minimize runtime errors enough to work well. It would then appear that static type systems are demonstrably redundant for this purpose - catching failing programs before runtime - in most cases.

In my experience, they are more useful for (a) describing the API in a machine-readable way between different modules of a system which are developed independently, and hence have to deal with versioning problems over time, and (b) aiding program modification by letting the programmer state more invariants, in particular dependencies between one part of the code and another, which in turn makes documentation, code browsing, editor code completion, automated refactoring, and indeed manual refactoring - change the code, recompile, then use the type check failures to locate the places that need to be updated for the new code - easier.

If we could get those things without static type systems, and without losing the benefits of flat text file representations of programs, we'd probably be happier. Unit tests fit the bill well in some cases, poorly in others. But I suspect a proper replacement would quack just like a static type system.

Ask yourself, are you looking to advance your understanding of someone else's point of view, or trying to advance your own position. You can't possibly disagree until you understand what I am saying.

To me, most of the mistakes in Java were made pre-FJ. How does FJ help fix existing problems? What about C++? What about Ruby? Python? For a good example paper that touches upon flaws in Simula and Eiffel, see Fisher and Mitchell's Notes on Typed Object-Oriented Programming.

A lot of earlier object-oriented languages also committed the dreaded sin of arguing they were based on "strong typing", especially Smalltalk systems that added a type system to Smalltalk.

Oleg Kiselyov has some good examples of both bad design decisions for functional and obect-oriented languages (although, I think his casual remarks about OO languages are a bit much and misrepresent the problem in the effort to show what's wrong).

have you ever programmed in Self or Smalltalk?

Self, no.
Smalltalk, yes.

If evaluation rules aren't semantics, then what, in your definition is?

I think we're getting off-topic here, but what are you asking me for, really? Java did not have a memory model for a long time, but it still had threads and you could deadlock a system pretty trivially for a long time. The interactive, procedural attributes of OO languages make them very hard to give semantics for, especially with complex coordination mechanisms like threads. Sure, there were languages, like Sina (a distributed Smalltalk), that offered more robust concurrency and coordination primitives than threads.

I am not sure what you are getting at. If you took a program written in one of these typed OO languages and ignored the types and simply executed the program, it still would compute the same result.

Exactly.

After all, the purpose of a static type system, whether for the lambda calculus or for some OO language, is to reject programs that might fail at runtime.

I don't think a type system has to reject whole programs. Some people, for instance, use type errors as control operators [1] [2] [3]. I don't think this is a great use of a type system, but it has its use cases (e.g., exploratory programming).

[1] Adam Chlipala is quoted on LtU as saying he uses Coq type errors as control operators, but I am too lazy to search for the post.
[2] We can also implement "method missing" as a type error and provide a programming language feature that allows handling type errors as-if at "message binding-time". I don't like this for many reasons.
[3] I use this sometimes for small DSLs where I want a simple hackish way to signal a user interface about some constraint violation. The idea being the GUI allows the user to compose functionality in such a way that they are programming, and so type errors may need to be resolved before computation can propagate through the system. This is not far off from Gilad Bracha's vision of IDEs having multiple type inference engines for a given language with pluggable types, except I have not formalized it yet. See my comments above about "a crucial misconception" and how it seems to apply to Mirah and its coupling of Ruby syntax to type inferencing.

It is a slippery notion, the separation between language and library. And within the language, delineating exactly what is in the runtime versus what is inherently in the "core language" is even harder.

Mirah only relies on the libraries that come with the JVM, as opposed to languages that carry along a few dozen megabytes of potentially conflicting libs.

Thank you for explaining. It seems I was misreading the statement, then, or that it should have said 'no runtime dependency other than the JVM and invoked libraries'.