# What are the guiding design principles for designing programming languages that allow Sketching?

I wanted to implement and design my own programming language that allowed sketching, like Combinatorial Sketching for finite programs. I was reading through the paper but it was unclear to me if there were general principles or techniques for doing such a Sketching design (especially wrt to programming languages that already exist, say extent, python, C, Java, Coq, Mizar, etc with these capabilities).

Can one extract such principles from the paper?

In particular so that QBF is applicable i.e. Quantified Boolean Formula Satisfiability Problem (QBF) and a sketched (partial) program $$S$$ with specification $$P$$ and control (i.e. wholes to fill) $$c$$ satisfy the following:

$$\exists c \in \{ 0, 1 \}^k, \forall x \in \{ 0,1\}^m ; P(x) = S(x,c)$$

for completing sketches.