Vala a modern language for embedded, validated with VCC for C?

I'm always in search of the mythical 'Silver-Bullet' language that will let all of us write bug free software for our Embedded Systems. This week I came across Vala. Vala is a new programming language that aims to bring modern programming language features to GNOME developers, its syntax is taken from C# amd Java. What piqued my interest is that Vala is a front end that compiles to native C code. So there is some hope that it would be run on an Embedded Micro, tho it would have to have some beefy memory to support GObject.
Some of the features of Vala are:

• Assertions and Contract Programming.
• Signals/Asynchronous Methods; With asynchronous methods it is possible to do programming without any blocking. [Yes, the masochistic could do this with raw function pointers.]
• Anonymous Methods / Closures.
• Multi-Threading.
• Resource Control.

Still there are a few kinks I see in Vala. The Vala Tutorial gives some examples of where the language will let you shoot yourself in the foot. A language should do all it can to prevent errors by the programmer. If we want to use a language that lets us shoot ourselves in the foot we can keep using forty year old C, or Programming A Problem-Oriented-Language by Charles H. Moore, written ~ June 1970.

I don't know how close Vala's asynchronous queues are to a true message passing system like Erlang. Hopefully close enough to have to avoid the whole issues of threads and locks, but I don't think this is the case from look at a bit of the code. Threads and locks simply do not scale, especially after you get past about 64 cores. Linux multi-core scalability is a good paper to start with on the issue. I'd like to see a language similar to Vala that enforced single assignment variables and true message passing, that complied down to something that ran on our small micros.

Chips with 144 independent F18A computers are just starting to come on the market now, so we collectively need to get our acts together on doing multi-core programming, without archaic notions of shared variables, threads and locks.

Something else I came across this week over at CodePlex was VCC from Microsoft: "VCC is a mechanical verifier for concurrent C programs. VCC takes a C program, annotated with function specifications, data invariants, loop invariants, and ghost code, and tries to prove these annotations correct. If it succeeds, VCC promises that your program actually meets its specifications."

I wonder how you could convince Vala to output VCC annotated source code to feed VCC to prove a 144 core program is correct on one of Chucks Chips? I do realize chips from Chuck Moore will be using Forth...