Lambda the Ultimate

I question whether Ada can rightly be regarded as "safe" with such functions as UNCHECKED_DEALLOCATION (which, incidentally, is one of the tricks needed to make Ada truly fast).

Incidently, an Ada implementation can make use a of garbage collector, by the way (say on CLR, or the JVM) and then one doesn't need to manually release memory.

Doesn't the possibility of dangling references violate safety, since the types of pointed-to objects can no longer be guaranteed? BTW, "permitting GC" (as opposed to "requiring GC") is a red herring, because even C++ is compatible with the Boehm collector, and nobody in their right mind would call that a safe language. Let me illustrate what I believe is a lack of Progress (in C++, though it should be trivial to translate to Ada...it's been nearly a decade since I touched the language):

1) int* x = new int(5);
2) int* y = x;
3) delete x;
4) *y;

Now I claim that the semantics of line 4 are undefined in both C++ and the equivalent Ada program. And if they are undefined, then progress fails at line 3, because there is no proper way to evaluate line 4 (as in, evaluating line 4 does not yield a well-defined value according to the language semantics). If I've misunderstood type safety, I'd be glad to review a good reference (though it's hard to find a good one online).

Forget about the corporation for a moment. Do the technical ideas make sense?

...even if they aren't terribly novel. (Which isn't a bad thing, necessarily). Compiler verification of contracts (invariants) is always an interesting problem, and the "Software Isolated Process" (a single-threaded, dynamically-compiled VM instance essentially) is an well-known concept--a straightforward extension of what the CLR or JVM currently does.

In further praise of MS, I'm happy to see that shared state concurrency appears to be banished from the model. While Sing# isn't a single-assignment language like Erlang, this is a welcome step away from a programming model which is a notorious source of bugs.

That is what I'm wondering, and in case you haven't already noticed, I'm a total n00b. So I can't answer.

What is the price of message based communication between processes?

On page 6, what is meant by "...applications as a security principal..."? And how would that be different from "user permissions"?

Application Manifests sounds *super cool*. Does this really mean, easier installation, better dependancy management, and cleaner un-installs?

How truthful is it that, "faulty device drivers cause 85% of diagnosed Windows system crashes"?

If we're going to object to the inheritance of ideas from other languages, then we might as well discount concurrent Haskell as well - it lifts many of its ideas from occam, including the notion of ultra-lightweight processes that can only communicate via type-safe channels.

So why not just implement everything in occam? Well, mostly because Haskell has all sorts of neat features that simply aren't available in occam. More to the point, it's silly to object to the idea that one programming language can't learn from another one. Our ultimate objective is surely to improve PLs in general. That's inevitably going to involve inheriting ideas from other languages.

and Equal Opportunity Admiration, for example Autrijus' Visual Basic Rocketh talk at EuroOSCon.

I will never be a language snob, only a feature snob!

Type safe channels (like Occam) is not the same thing. Haskell being a functional language means the channels are typed and higher-order... You can declare a channel where the types are function types (And that is types, not function pointers which are untyped). Haskells light-weight processes are not the same thing either, they come for free from the nature of the spineless-tagless-graph-machine that is the core of GHCs implementation, whereas Occam's come from having many transputers running in parallel. Occam, AFAIK when running on a single CPU has the same overheads associated with threading and processes as any other language. The light-weight processes in Haskell are like threads that have the separation of processes - in other words they run in the same address space, but the type-system guarantees they will not interfere with each other, and this condition is prooved at compile time. Singularity includes the higher order nature of channels and the type-system driven light weight processes. So again the emphasis is on the static proovability of properties - something which Haskell does already - and nothing like Occam. Remember Haskell was developed by a pooling of functional talent - to put a stop the the over-proliferation of different languages all trying to implement the same typed-lazy-functional paradigm. So if C# is developing into another typed-lazy-functional language they should do the right thing and use Haskell ...

Perhaps I distracted you from my point by focusing on Haskell. What I really meant to say are all these things are such that they come for free (or practically for free) in a functional language like Haskell. In other words functional languages are the natural domain of expression for these kind of ideas...

I can see nothing new here - except the application of ideas from functional programming to C#... which looks like prior art incase they try to file for any patents. Perhaps C# will take on so many idea's from functional languages it will eventually become more functional than imperitive...

As for language snob - That was my point... It seems some people are too busy evangelising C# and adding features to see that what they will end up with is already available (IE Haskell has a mixed functional/imperitive model, using Monads to encapsulate the effects of the imperitive sections).
Why not just use the other language that provides the features. If you turn visual-basic into Pascal, would it not have been better just to use Pascal? VB's main competitor was Delphi (which is Pascal), until they poached Delphi's lead developer, who is responsible for some of new ideas. Also MS employed former academic Erik Meijer who brought his work on HaskellDB to C# and VB. So perhaps these changes were not unpredictable. I think what makes me uncomfortable is that MS is paying people to recreate and carry on work started in other languages - but ontop of the .Net platform.

You could almost say they are _embracing_ these ideas... Linq also _extends_ the ideas in HaskellDB by applying them to XML and objects (a fairly obvious extension - but cool too). We all know what follows "embracing and extending..."

I appreciate the point about improving all PLs, so the relavent question I suppose is "what does this add"... and thats where the relavence of my comments should be obvious - we already have most of this. The ideas in Spec# and Sing# may be interesting. However I don't like the idea of two separate languages - so this gives me a direction to progress this... Is there a single language that could replace both C# and Sing#, a language capable of writing both the specification and the implementation?

Haskell being a functional language means the channels are typed and higher-order... You can declare a channel where the types are function types (And that is types, not function pointers which are untyped).

Haskells light-weight processes are not the same thing either, they come for free from the nature of the spineless-tagless-graph-machine that is the core of GHCs implementation, whereas Occam's come from having many transputers running in parallel. Occam, AFAIK when running on a single CPU has the same overheads associated with threading and processes as any other language.

What I really meant to say are all these things are such that they come for free (or practically for free) in a functional language like Haskell. In other words functional languages are the natural domain of expression for these kind of ideas...

I agree with most of that... Except it ignores elegance... Sure you can bolt any feature onto any language (almost... I think if you model language features as monad-transformers you find that some features exclude certain other features) but will you not end up with a frankinsteins-monster? Some features have a synergy... and these features seem to me to be much happier in a functional languge than a derivative of C/Java/Pascal. The most elegant ideas derive all the required features from a few simple core ideas.

Of course it is great that microsoft are doing this, and its always good to see good ideas being adopted. I don't dispute this - but thats a different question from is this the best way to clean-room produce a secure operating system.

Dont forget Hos and House, a Haskell based OS that boots on PC architecture and has some (I haven't read enough about Sing# to know if all its properties could be simulated by type-level logic programming with type-classes in Haskell) of the same features for free just because its written in Haskell. To be fair it could probably be in ML or Clean just as well.

Any ideas about combining the specification language and the implementation language?

Any ideas about combining the specification language and the implementation language?

Perhaps the best option is to provide a kind of meta-specification/implementation language, which can be used to develop domain-specific specification/implementation languages. I have no idea what that would look like, although there may well be some clues in HasCASL since CASL itself has been extended to encompass a variety of other formalisms (including LTL, CSP, and state-based approaches).

Indeed, that is in principle what CASL is supposed to be: a base specification language upon which you can build various different domain specific languages. It is, in a sense, designed to address precisely the issue that no one specification langauge can really suitably address all the different domains without becoming tortuously convoluted and unusable. Instead it aims to provide a common basic structure upon which different formalisms can be elegantly constructed in a consistent way.

There is good theoretical underpinning for this too - there is a lot of work on the theory of institutions which provides a framework in which different logical systems in a meta-theoretic way and transfer general results across into new systems. I'd reccomend the paper by Andrez Tarlecki on the subject which provides a nice introduction to the framework.

And low-overhead, secure concurrency comes for free in a language designed from the ground up for it. Like occam. Which makes occam the natural domain of expression for those kind of ideas (especially given occam's close ties to CSP semantics). So why add those kind of features to Haskell (which has a semantics much closer to the λ-calculus than the π-calculus)? By your logic, it should never have happened.

Because in Haskell's case there aren't any features that really want taking out - there's an embedding of the λ-calculus into the π-calculus, and Haskell is already adept at turning itself into λ-calculus-embedded-into-something-else.

To put it another way, Haskell's a natural domain to start building other ideas in because it tends not to get in your way with existing features that interfere. Me, I just wish people'd talk about (denotational) semantics more and category theory (as a Big Thing) less - that's where the magic lies.

(not that I disagree with your post, just explaining some of the original logic)

Just one at a time. I've had systems of up to several million processes running at one time, on one processor, in the same address space. Statically proven not to interfere with each other.

How much memory did the millions of processes take up? I recall a post on the Erlang list talking about topping out at 1.8 million processes before running out of addressable memory. At 1Kb per process that's close to 2Gb.

Predictably our processes have grown a heap and the heap has been used to implement a stack. So it goes.

A note on the erlang mailing list about Mnesia and running millions of processes on a 16GB Sparc:

http://forums.trapexit.org:81/phpBB/viewtopic.php?t=5429

With the disk arrays we do blow out to 8U of rack space for a full cluster but it still looks comical compared with the racks and racks that make up Java/Oracle systems at these sites :-)

That link is broken. This should work better:

http://thread.gmane.org/gmane.comp.lang.erlang.general/12518/focus=12521

How much memory did the millions of processes take up? I recall a post on the Erlang list talking about topping out at 1.8 million processes before running out of addressable memory. At 1Kb per process that's close to 2Gb.

You said "You can declare a channel where the types are function types (And that is types, not function pointers which are untyped)."

Why do you say that function pointers are untyped?
In C, you cannot assign a function address to a function pointer with a different prototype, so they are "typed", weakly of course as it is C but typed nonetheless..

Okay... I guess thats my mistake - I guess I really meant weakly typed. In an attempt to justify myself though, the point of typing a channel is that you get a strong guarantee that the function passed will not cause an error. Allowing a function type to be cast removes this guarantee - so I would argue that in this case (as in any where you are looking for provable correctness) allowing a cast is as bad as no type at all.

This explains some of the weirdness I felt at the thought of extending a language with casts to have design by contract. I guess C# is somewhat better than C by forcing you to declare such code unsafe... but as unsafeness is not protected by the type system its not much better than C really. Presumably one of the features of Spec#/Sing# is to restrict the use of unmanaged code. It would be better if C# used monads and could therefore require any function using unmanages code to be in the Unmanaged monad... thus a function could be restricted from running unmanaged code by the type of the calling function.