[bitc-dev] C interfacing vs. portability

[Jonathan S. Shapiro]

On Thu, Feb 26, 2009 at 6:03 PM, Jonathan S. Shapiro <shap at eros-os.com> wrote:
> Range constraints incur a discharge obligation. In the general case,
> this is an unsolved problem in the literature.

Before I forget to say this...

There is a meta-level problem with constraints. Success at discharging
them is a function of your prover, and nobody seems to have any way to
specify what things a prover is *obligated* to prove, nor how to
satisfy such an obligation. In consequence, there is no way that a
language specification can assure that "integer between 5 and 10" as
an obligation can actually be satisfied. This means that in general we
lose the ability to specify which programs are valid according to the
language definition.