I Want Spec#


Scott Hanselman has recently put up a new hanselminutes of an interview with the spec# team. This interview was done at altdotnet; one of the key points of discussion both in general and in the interview was “how can we get spec#?”. The simple answer is we have to want spec# and Microsoft needs to know that we want it. The more people who want it the more likely we are to get it or to get it in pieces. The best way for them to know is for us to tell them!


Let’s give Mike and the whole spec# team the best compliment possible on their research; asking for it to become integrated in products and/or to be available with a commercial license!

I want verifiable software…





Here is a reusable bumper sticker for your blog to make it easier to express how you feel.




Drop a note here so I can try to keep track of people!


If you don’t know about spec# now may be a great time to watch the recent presentation from altdotnet

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

38 Responses to I Want Spec#

  1. Pharme947 says:

    Very nice site!

  2. Pharmc252 says:

    Very nice site!

  3. SealedSun says:

    I’m a bit late but I want Spec# too!

  4. Raoul Duke says:

    I’d rather have a good form of dependent typing, that can subsume DbC. Heck, there are even people at MSR who are working on Ynot/Coq.

  5. A Dropper says:


  6. Specsharp discriminates between expressions that may evaluate to null and those that are sure not to. It will greatly reduce errors inherent in modern programming languages.

  7. Glenn says:

    Your readers might be interested in a soon to be released collaborative project life cycle management web application that captures requirements and tracks the coverage of requirements all the way through analysis, design, development, and deployment. You can sign up for the private beta at http://www.dynamicalsoftware.com/beta.html or just download the white paper at http://www.dynamicalsoftware.com/clicksppm.html

  8. Dean Grossmith says:

    Yes to DbC – there is so much anecdotal evidence out there that says it leads to better quality sofrware.

  9. David Kreth Allen says:

    I want DbC.
    And if it is not ready yet for prime-time as a first-class language feature, you could add Spec#-like features to Code Analysis warnings. Who cares if it misses a few edge cases? I’d be delighted to detect null dereference possibilities in 95% of the cases. Finding and fixing those translates to real observable product quality improvements.

    With software as complex and large as it is today, we MUST get more automated help to detect defects early in the lifecycle.

    At least make namespace Microsoft.Contract public so I can borrow your PreconditionExceptions and so we can start to manually code some DbC using some pseudo-standard language.

  10. Robin says:

    I want Spec#!

  11. Jimit Ndiaye says:

    Need! Want it! Gotta have it! A.S.A.P.!!! And not just in C# either… i need it baked into the BCL and CLR so it’s usable in .NET languages other than C#

  12. Stewart Rogers says:

    I love Spec# and I must have it.

  13. Kevin McFarlane says:

    I want Spec#!

  14. Sadek Drobi says:

    +1 for DbC
    +1 for spec#

  15. Simon Segal says:

    I must have spec# (sooner the better).

  16. Greg says:

    Henry you are correct dynamic languages and compile time proving are pretty much mutually exclusive.

    I had a great chat with the Mike and Rustan from the spec# team and John Lam from the IronRuby team on how the two can play nicely together since each has its own strengths and weaknesses. I recorded this chat and should be putting it out sometime soon.

  17. Hendry Luk says:

    The way i see it, spec# is the exact opposite of ruby. It’s quite fenomenal the recent hype about Ruby, enthusiasm to get similar duck-typing-ness on CLR, while at the same time we’re also fancying spec#.
    Im not a fans of Ruby to begin with. So, go spec#!!

  18. Hendry Luk says:

    I am wondering if there has been any work done on compile-time DBC based on C# attribute? How possible (or impossible) is it?

  19. Kyle Lanser says:

    Just read a couple of the PDF’s on http://research.microsoft.com/specsharp/ and DbC looks awesome!
    Need to get more people talking about this!

  20. Jeff Tucker says:

    I want spec# and the chick wearing the T-shirt

    blogged: http://agilology.blogspot.com/2008/04/i-can-haz-spec-kthx.html

  21. Greg says:

    Kim: BCL + DbC + compile time proving = me very very happy :)

    btw: its good to see that you have been moving that direction with new development using Microsoft.Contracts.

  22. Kim Hamilton says:

    It’s well known that BCL wants Spec# so we can get some DBC goodness in the framework libraries!

    (I wouldn’t mind having that t-shirt too…)

  23. I thought someone from the C# team should chime in here and let you know we are following this thread and that we are aware of the interest in Spec#. There is nothing to announce at this time, but I wanted to let you know that you are being heard. I’ve seen a few emails going back and forth about this, and of course their are Spec# fans on our team who share your passion for this subject.

    – Charlie

  24. Also want to have spec#!!!

  25. Mike Strobel says:

    I forgot to mention that the Nemerle language now has partial support for Spec#-style contracts, but it does not yet have static analysis support. There’s also no support for expression trees or LINQ as far as I know. Maybe some kind soul with a nice chunk of spare time would be interested in bringing the language up to speed?

  26. Mike Strobel says:


    That’s reassuring to hear. At least it sounds like we’ll end up with some form of DbC support. I actually did some experimenting a couple weeks back using the Spec#-generated attributes in C# code and running Boogie against it as a post-build process. It actually worked pretty well, but the expression syntax for those attributes is pretty cumbersome and not very practical to use outside of Spec#.


  27. Todd D says:

    want it, want it, want it! it’d be so much better not to have DbC stuff infiltrating my code at runtime

  28. Yes, DbC in C# as soon as possible!

  29. RhysC says:

    I want it now!

  30. Steven says:

    Love it, need it, want it!

  31. Eyad Salamin says:

    I love it and want it.

  32. deerchao says:

    I love Spec# and want it too.

  33. Greg says:

    Mike, I have had those same conversations …

    Actually I think some of them are in that video … if not they are in the interview I did with Mike and Rustan for infoq.



  34. Mike Strobel says:

    A past informal conversation with a member of the C# team has left me with the impression that we’re unlikely to see Spec#-style language support for DbC constructs in a future version of C#. It seems we’re more likely to see DbC support in the form of a framework that works across .NET languages, coupled with some sort of static analysis support. While I would naturally love to see C# include native DbC support (or Spec# to include the C# 3.0 language features), I’d be pretty reasonably content with solid DbC support in the form of assertion methods and attributes.

    On a side note, I’ve created a feature request on the ReSharper issue tracker to add realtime/compile-time static analysis of DbC constructs in a future release of ReSharper. I posted a link in the R# community forums, so anyone who’s interested is encouraged to vote for the feature.

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>