Verve: A Type Safe Operating System

Sign in to queue

The Discussion

  • User profile image
    exoteric

    UACK! . My wet OS dream. Must watch...

  • User profile image
    Chris​Stepaniuk

    @exoteric: ha!  I haven't even watched the video yet and was thinking the same thing, type-safe operating system.... booyah!

  • User profile image
    Charles

    I recommend that you read the paper and then watch this. The gory details are in the scientific literature. The goal of this conversation was to explore the thinking behind this research project. Of course, as usual, this is a conversation, not a presentation. My random questions aren't too random (I read the paper before we chatted). I like how this turned out. A little long, yes. But there are many good nuggets in this one. Hunt for them, Niners! Use your minds.

    C

  • User profile image
    Mr Crash

    erm didnt you say in the video that Verve was available on codeplex or did i miss-heard ?

     

    btw: is the codeplex "The Singularity project" dead ? have been no activity for a long time  Sad

  • User profile image
    Charles

    , Mr Crash wrote

    erm didnt you say in the video that Verve was available on codeplex or did i miss-heard ?

     

    btw: is the codeplex "The Singularity project" dead ? have been no activity for a long time  Sad

    You heard correctly. The Singularity Project is more than a single thing (so saying "it's" dead is somewhat meaningless...) I mean, there would be no Verve project without the Singularity research findings. In some sense, Verve is a natural, though with different specific focus (e.g., fully verifiable operating system, typed AL, managed HAL (Nucleus), etc), evolution of the Singularity project. The important point is that OS research is alive and very well both inside and outside of MS. Verve, like Singularity, is about exploring fundamentals and rethinking the OS stack. Also, as is the case with Singlularity the OS, there is no product trajectory for Verve. It's basic science, not product development...

    Here's the link to source code: http://singularity.codeplex.com/SourceControl/changeset/changes/45126

    C

     

  • User profile image
    Mr Crash

    @Charles:
    From: http://singularity.codeplex.com
    "Committed On: Sun May 16 2010 at 2:45 AM"

    Need i say more ?  Expressionless


    Where's the updated code ?

     

  • User profile image
    felix9

    wow, its indeed an impressive project, it looks like verifiable software stack is not too far away.

    thanks Charles.

    now lets wait to see the 'C3' paper from Wolfram Schulte etc, maybe a verifiable web platform ?

  • User profile image
    exoteric

    Great interview, Charles. Now onto the research paper. I wonder if this has something to do with the iTALiX project, also comming out of MSR...

    https://research.microsoft.com/apps/pubs/default.aspx?id=121445

    Looks like it, same author!

  • User profile image
    Charles

    , exoteric wrote

    Great interview, Charles. Now onto the research paper. I wonder if this has something to do with the iTALiX project, also comming out of MSR...

    https://research.microsoft.com/apps/pubs/default.aspx?id=121445

    Looks like it, same author!

    Indeed. Chris and company have been working on TAL for a while now. It is certainly a very related project in this respect. For Verve, all of the code for the OS is statically verified when the system is built. The only unverified code in the system is the boot loader, which is fine in some sense because it only runs once and then is no longer executed... Even the GC is verified (I asked this question in the interview and he said it was or will be soon. At least, that's what I remember).

    It would be useful to learn more about TAL specifically. Perhaps we'll get Chris on 9 again ( E2E Smiley ) to go over the TAL stuff with a language expert..

    C

  • User profile image
    magicalclick

    I know I am asking redundent question. But, how likely and how soon in estimation would be seeing this in the market? I really really really hope to see this or Singularity in 5 years, but, I am also affraid MS will not take the step and waiting for competitors. I understand their marketing decisions, but, would I be able to see MS releasing Type Safed OS first in the name of practical science?

  • User profile image
    exoteric

    , Charles wrote

    It would be useful to learn more about TAL specifically. Perhaps we'll get Chris on 9 again ( E2E Smiley ) to go over the TAL stuff with a language expert..

    C

    It would indeed. I think we'd all love to hear more about the TAL.

  • User profile image
    Rukur

    Thanks for your time Chris. I hope you push Verve further into a real OS.

     

    Look forward to hearing more.

     

  • User profile image
    reidgisel

    This is intresting.It shows that M$ spends on research.Renaissance for assembler maybee?

  • User profile image
    B3NT

    the interesting thing about this, to me, isn't even that it's an OS, its the use of Z3/boogie as a prover...this speaks directly to turings halting problem. these guys have the coolest job on the planet.

Add Your 2 Cents