How do people define (gensym) in the context of (first-order) logic? I want to say something like > Let θ be a renaming substitution such that the variables in vars(range(θ)) have never been used before, and cannot be produced by any other means or, well, you get what I mean, right?

I can at least say they are different from all variables of a given formula and other variables appearing elsewhere explicitly, but it would be much simpler and less error-prone if I could say something like “They’re unique like a (gensym)”

In informal contexts, people sometimes say things like x is fresh, which stands for the “you know what I mean” you say above. (The rigorous logician’s response might be that sometimes people don’t know what they mean.) But in formal contexts, I don’t know of a simple way to avoid specifying what the variables are fresh with respect to. You might be interested in “nominal logic” (from Andrew Pitts), which extends first-order logic with a freshness quantifier, but I don’t know whether it would be helpful in your case. For example, if you have two freshness-quantified statements, what are the rules for combining them? And is it clearer to rely on the logic’s additional rules than to explicitly write the set constraints in the propositions?

Thanks Ryan. Yeah, I don’t really want to extend the rules of logic indeed. So I guess I’ll just have to bite the bullet of verbosity. For now I could mitigate it somewhat with something like: > A freshing substitution θ for a set of variables V within an underlying enclosing formula F is such that … and vars(range(θ)) \cap vars(F) = ø. And then I add additional constraints when I need several freshing substitutions at the same time.

Because a contract can be an arbitrary predicate, which makes equality between contracts undecidable in general (I think) does that make it difficult to perform static analysis on contracts?

I would say so, yes. Plus, people tend to write convenience functions for constructing contracts. It can be difficult to get those convenience functions and static analysis to communicate with each other.

Hm, maybe if there were certain restrictions on contract combinators and wrappers, it’d be possible to make static analysis more tractable…

I know that’s not something that can be done in #lang racket, but it would be possible in a new #lang.

There’s a bunch of research on static analysis of contracts

It’s not obvious that a plausible set of restrictions would make that much difference

Figuring out what the contract is usually isn’t the hard part

What makes it tricky?

My guess was that, since Racket’s contract can be Turing-Complete, it would complicate things, but it appears that my guess was off.

The hard part is figuring out what the program does — first class contracts with arbitrary predicates add some extra complexity but the underlying problem is plenty hard.

Could you elaborate on, “figuring out what the program does”? Do you mean in the sense of a formal specification?

I mean in the sense that you have to check if the program follows the contract, which requires analyzing the program itself.

Oh, so it ends up being a problem of symbolic execution?

well, there are lots of ways to analyze programs; symbolic execution is one