BOUNDP checks free variables in PROGV?

Suppose both a and b are unbound (i.e. (notany #'boundp '(a b)) => T), then this works as expected:

(progv '(a b) '(1)
  (boundp 'a)) ; => T

Then PROGV entry in CLHS states:

> If too few values are supplied, the remaining symbols are bound and then made to have no value.

which contradicts what I see in REPL:

(progv '(a b) '(1)
  (boundp 'b)) ; => NIL

I'll expect (boundp 'b) to return T.

Question: Did I misunderstand the wordings in CLHS? Or is it a bug in SBCL?

Environment:
SBCL 2.2.10, Linux x86_64

Thanks!

I think the wording in the standard is poor, but what is intended to happen is that

(progv '(a b) '(1) ...)

is equivalent to

(progv '(a b) '(1 nil)
  (makunbound 'b)
  ...)

This is very different than simply not binding b at all as you can see by considering this:

(progv '(b) '(3)
  (progv '(b) '()
    ... b unbound here ...)
  (symbol-value 'b))

which evaluates to 3. The issue is that makunbound removes the value of the dynamic binding of the symbol that is currently in scope. In a shallow binding implementation that's the same thing as simply marking the value cell of the symbol as having no value, because the outer value will be restored in due course. But in a deeply bound implementation the binding must still exist in the stack of bindings, but its value must be marked as 'unbound' somehow.

Perhaps the problem, really, is that boundp and makunbound at least are arguably misnamed: boundp really tells you if the current dynamic binding of a symbol has a value, not if one exists at all, and makunbound removes the value from the current dynamic binding. But these names were inherited by CL. There is no way of telling (and probably should be no way) whether there is a current non-global dynamic binding for a symbol or not.

Finally, this behaviour of progv is useful because it means you can say

(progv '(a b c) '()
  ... now I know a, b, c are unbound ...)

which means you can avoid the problem that somebody might have polluted the environment in ways you can't control.

It states first bound but then made having no value (means not even NIL as a value - what I think you expect - me too, because that would be the behavior in lambda lists e.g.). So then b must be unbound after binding (like (makunbound 'b)). Only after being unbound, variable b would have no value.