gsps

As far as I understand, their approach is exactly that, i.e., another target language for extraction. Synthesis is a bit of an overloaded term.

If you're interested in declarative programming, you should also have a look at answer set programming. Here's an ASP version of the problem that additionally requires prime factors.

  domain(100..999).
  digit(0..9).
  
  % Variation w/ prime factors
  prime(P) :- domain(P), { domain(F) : F < P, P \ F == 0 } 0.
  prod(P1 * P2) :- prime(P1;P2).
  
  % Palindrome
  pd(X) :- prod(X), X = 100000*A + 10000*B + 1000*C + 100*C + 10*B + A, 
    digit(A;B;C).
  
  pdMax(M) :- M = #max { X : pd(X) }.
  #show pdMax/1.

Superficially it resembles Prolog, but brings "true" declarativity to the table, i.e., the order of rules and the order of atoms in the body is negligible. Various notions of safety and the prohibition of nested complex terms (e.g. `f(f(x))') guarantee termination. Most importantly though, solutions to an answer set program are not proofs (as in Prolog) but truth-assignments of atoms ("answer sets"). In this specific encoding there's no significant difference though, as we're only computing a single answer set containing an atom "pdMax(X)" with the maximum palindrome X.

Solving answer set programs usually involves heuristics and much work along the lines of SAT solving. Recent solvers such as clasp [1] are surprising efficient though and rival state of the art SAT solvers.

[1] http://potassco.sourceforge.net/