Rosette – A solver-aided programming language that extends Racket

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.

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

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

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