For more on Rosette I recommend watching Emina's keynotes at the (sixth RacketCon) [0] and Clojure/west 2017 [1].

[0]: http://con.racket-lang.org/2016/#speakers

[1]: https://www.youtube.com/watch?v=KpDyuMIb_E0&index=25&list=PL...

Nice! For constraint solving, I can also highly recommend to look into Prolog for some useful ideas.

For example, consider the use case of Rosetta that is shown on the page. In Prolog, we can express it as follows: First, let us define suitable operators, so that we do not need so many parentheses:

    :- op(200, fy, ∧).
    :- op(200, fy, ∨).
    :- op(200, fy, ¬).

With these definitions in place, we can implement the SAT solver that is shown on the page as follows:

    sat(F) :- interpret(F, t).

    interpret(∧Ls0, T) :-
            maplist(interpret, Ls0, Ls),
            apply(and, Ls, T).
    interpret(∨Ls0, T) :-
            maplist(interpret, Ls0, Ls),
            apply(or, Ls, T).
    interpret(¬Expr, T) :-
            interpret(Expr, T0),
            not(T0, T).
    interpret(t, t).
    interpret(f, f).
    interpret(v(f), f).
    interpret(v(t), t).

    apply(and, Ls, T) :- foldl(and, Ls, t, T).
    apply(or, Ls, T) :- foldl(or, Ls, f, T).

    and(t, t, t). and(t, f, f). and(f, t, f). and(f, f, f).

    or(t, t, t). or(t, f, t). or(f, t, t). or(f, f, f).

    not(f, t). not(t, f).

Thus, we can post:

    ?- sat(∧[v(R),v(O),∨[v(S),v(E),¬t], v(T), ¬v(E)]).
    R = O, O = S, S = T, T = t,
    E = f ;
    false.

On backtracking, all satisfying assignments of variables to truth values are reported. In this concrete case, there is only a single solution.

Interestingly, the Prolog version can not only be used to find satisfying assignments, but also to generate whole formulas that evaluate to true:

    ?- sat(F).
    F = ∧[] ;
    F = ∧[∧[]] ;
    F = ∧[∧[], ∧[]] ;
    F = ∧[∧[], ∧[], ∧[]] .

However, this particular enumeration is called unfair, since there are true formulas that will never be generated.

The coolest thing I saw in the applications page is the Chlorophyll DSL compiler for Chuck Moore's green arrays many-core Forth chips.

Ohh you're teasing me.

Here's the tease:

https://www.youtube.com/watch?v=zMfdef-nYGY

Thanks a ton. IIRC GA aren't that expensive. . might be fun to spend some money on this.

Amazing. Is the Forth interpreter / compiler from Green Arrays?

The DSL is a Berkley project:

http://pl.eecs.berkeley.edu/projects/chlorophyll/

Could this be added to Hackett, creating, perhaps, Hosette? [1]

1. https://lexi-lambda.github.io/blog/2017/05/27/realizing-hack...

You might be able to use Rosette to implement refinement types on top of Hackett, giving you (I guess?) Liquid Hackett.

Great stuff, love the names for some of the applications, especially Bagpipe.