Altdotnet Spec# Session

Here is another video in the videos from altdotnet. We had Rustan and Mike of the spec# come out from their cave (j/k) at MSR to talk about spec#, boogie, and the future of compile time proving!



Enjoy it and as always feel free to leave feedback! 


 the video is not the best quality but hey … it was taken on a phone!

This entry was posted in contracts, dbc, spec#, video. Bookmark the permalink. Follow any comments here with the RSS feed for this post.

57 Responses to Altdotnet Spec# Session

  1. jeson says:

    Thanks ,great article!

  2. jeson says:

    Thanks,great article!

  3. All I can say is Rustan and Mike are two of the coolest guys I’ve met!


  4. intro for the uninitiated on spec# and compile time proving.

  5. this is great knowledge!!

  6. chrystinad says:

    peter states caused measurements

  7. dannellski says:

    high indicate america controls arrives worldwide [url=]less due service new[/url]

  8. you decision makers up

  9. dfdads says:

    Yeah this is definitely an awesome intro for the uninitiated on spec# and compile time proving.

  10. I have read this post. This is very much true. Even I own a blog account on video conferencing. Video conferencing is indeed a great innovation in technology and communications. One day video conferencing will be like an ordinary house-hold item in the next 5-10 years.I will mention your post in my blog.

  11. Vicente says:

    I agree with Karl. I am looking foward to seeing this in the IDE.

  12. Nice video … thanks for sharing…

  13. Karl says:

    I have been wondering about this fact for a couple of years now. Why doesn’t C# support DbC? I think this would be _the_ most powerful feature in C# since the introduction of generics. I can’t count the various subtle errors in my programs which could have been avoided by using something like spec#.

  14. Greg says:

    Yeah this is definitely an awesome intro for the uninitiated on spec# and compile time proving.

    I agree that the two work very well together (this was actually my talk at devTeach last year). It does however become interesting in terms of TDD. Red green refactor really has another step if I put prover errors as compile errors … and it leads to a contract first mentality which I think is more appropriate in both a staticly verified language or even just a staticly typed language.

    test first works best in dynamic languages that let me call methods that don’t exist yet.

  15. Peter Gummer says:

    Everyone should watch this! It’s a really good presentation of the value of Design by Contract to the uninitiated.

    Having recently watched the Bertrand Meyer interview at, it’s amazing how C# is so far behind Eiffel in this respect. Eiffel has had contracts forever, and is currently in the midst of the move to not-null types. (And Eiffel is a .NET language too, of course.) The static verification in Spec# sounds great though. We’ve gotta get his stuff into C# now!

    One surprising thing about the presentation was that there didn’t seem to be any nay-sayers among the test-driven developers in the audience. DbC and TDD gurus are often hostile to each other, which has always bewildered me because it just seems obvious that the two approaches are complementary. Maybe the presentation was just too compelling for such doubts.

    Shame we didn’t really get to see the projected code in the video, but nice job with the camera phone all the same, Greg :-)

  16. Sorry for my bad holding at times, I was trying to figure out how to zoom… 😀

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>