[PRL] Re: Singularity project at MS

[Daniel Pinto de Mello e Silva]

On Fri, 2005-12-09 at 09:02 -0800, Paul A. Steckler wrote:
> > It has been on my reading list for a week or so. When I read the 
> > abstract, I thought I was re-reading the Matthew-Olin-Druschel-me ITR 
> > proposal from 99/00. -- Matthias
> 
> Is Singularity a Lisp Machine in a C#, OO guise?
> 

But it won't be limited to a single high-level virtual machine (in their
case running MSIL+) for very long.  In his presentation, he mentioned
ongoing work with typed assembly language and their technical report
says:

"In the short term, Singularity relies on compiler verification of
source and intermediate code. In the future, typed assembly language
(TAL) will allow Singularity to verify the safety of compiled code [36,
38]. TAL requires that a program executable supply a proof of its type
safety (which can be produced automatically by a compiler for a safe
language). Verifying that a proof is correct and applicable to the
instructions in an executable is a straightforward task for a simple
verifier of a few thousand lines of code. This end-to-end verification
strategy eliminates a compiler—a large, complex program—from
Singularity’s trusted base."
ftp://ftp.research.microsoft.com/pub/tr/TR-2005-135.pdf


Daniel