in Search

Do you Twitter? Follow us @CodeBetter

Greg Young [MVP]

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!

Published Apr 26 2008, 04:13 PM by Greg

Comments

Fervent Coder said:

Sorry for my bad holding at times, I was trying to figure out how to zoom... :D

# April 26, 2008 5:33 PM

Peter Gummer said:

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 http://channel9.msdn.com/tags/Eiffel, 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 :-)

# April 27, 2008 1:03 AM

Greg said:

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.

# April 27, 2008 2:02 AM

Jason Haley said:

# April 27, 2008 10:49 AM

Matthew Podwysocki said:

During ALT.NET Open Spaces, Seattle, I spent a bit of time with Rustan Leino and Mike Barnett from the

# April 28, 2008 7:21 PM

Matthew Podwysocki's Blog said:

During ALT.NET Open Spaces, Seattle, I spent a bit of time with Rustan Leino and Mike Barnett from the

# April 28, 2008 7:24 PM

I Want Spec# - Greg Young [MVP] said:

Pingback from I Want Spec# - Greg Young [MVP]

# April 28, 2008 7:27 PM

DotNetKicks.com said:

You've been kicked (a good thing) - Trackback from DotNetKicks.com

# April 29, 2008 12:53 AM

Links Today (2008-04-29) said:

Pingback from Links Today (2008-04-29)

# April 29, 2008 12:42 PM

Community Blogs said:

Hey , you decision makers up there at Microsoft. Maybe you didn't realize this, or maybe you're

# April 29, 2008 3:18 PM

Karl said:

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#.

# May 4, 2008 5:41 AM

Scott Hanselman's Computer Zen said:

# May 8, 2008 3:23 PM

ASPInsiders said:

My one-hundred-and-tenth podcast is up . This episode was recorded at the ALT.NET Open Spaces Conference

# May 8, 2008 3:27 PM

Name (required)

Your URL (optional)

Comments (required)

Remember Me?

Enter the numbers above:

Add

This Blog

Home

Syndication

News