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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.