Rosette – A solver-aided programming language

I always wanted to have clp, constraint logic solver facilities in regular languages. But I wanted all variables to be symbolic when used in clp context, and then just assert and support for = with lhs functions needs to be added. The trick is to find all symbolic variables involved by the compiler, but it's really trivial. cmbc does it e.g. for the C language. http://www.cprover.org/cbmc/

My plan is this: http://perl11.org/cperl/perlcperl.html#clp

    use clp;
    sub fact(int $i=0) :int { 
      assert $i>=0; return $i ? fact($i-1) : 1 }
    say fact(7);     # => 5040
    fact($_) = 5040; # solve it!
    say $_;          # => 7

Rosetta for example uses the typical simple LISP approach, by having to manually declare the symbols, which are being backtracked on. amb() is similar, expressing ambiguity. This goes back to 1963. http://community.schemewiki.org/?amb

I sort of understand the SDSL, but what is amazing is the diversity of the example implementations - verifying programs targeted eventually for the Greenarrays chips in Forth, and an OpenCL-based SDSL. Racket seems to be pushing outside the academic realm - almost.