Re: [boost] GSoC: Enforcing Code Feature Requirements

Subject: Re: [boost] GSoC: Enforcing Code Feature Requirements
From: Andrew Sutton (andrew.n.sutton_at_[hidden])
Date: 2010-04-03 09:00:31

I've also been thinking about similar relationships recently. Just a couple
of comments...

> The idea(s) is that concepts (ala C++) are a way to *verify* that the
> types passed in meet the necessary requirements.

> Unit tests are also a form of verification. So there seems to be a
> possible avenue of research here - using concepts as unit tests, or
> merging the 2 ideas.
>

I disagree that concepts are a method of *verifying* anything. Concepts only
*specify* constraints or abstractions. Verification is something that could
be done by a program checker, theorem prover, or test suite. Some people
want to aspects of verification into the compiler (e.g., Spec#), which turns
out to have some nice benefits.

> Unit tests are also a form of documentation.

No! Unit tests make terrible documentation. They're only incrementally
better than reading the class body, and only then because they might
demonstrate a particular order in which calls should be made or demonstrates
the invariants, preconditions, or postconditions that can't be proven.

> And concepts are also a form of documentation.
>

Only in as much as a class or function is "self-documenting".

> So they all seem to be interrelated.

Sure, but I think the more interesting relationship is between proof and
testing, and the elements of a language or program that enable either form
(or both!) of reasoning about a program's correctness. Documentation
somewhat of an orthogonal concern.

To try to tie this back into the original post :) Scott's article is
addressing the issue of improving verifiability through metaprogramming.
Think of the it annotating a function call. Of course, you're still have to
making claims about your program which need to be validated independently.
If those claims are valid, then (theoretically), any function you call
should also be valid under those stated assumptions. Very cool.

>
Andrew Sutton
andrew.n.sutton_at_[hidden]