Rosette – A solver-aided programming language that extends Racket • Hacker News Board

Rosette – A solver-aided programming language that extends Racket

#1

Post by tosh » Sun, Jun 04, 2017, 1:05 PM UTC

Rosette – A solver-aided programming language that extends Racket
emina.github.io

Re: Rosette – A solver-aided programming language that extends Racket

#2

Post by throwaway7645 » Sun, Jun 04, 2017, 2:27 PM UTC

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

Re: Rosette – A solver-aided programming language that extends Racket

#3

Post by agumonkey » Sun, Jun 04, 2017, 3:07 PM UTC

throwaway7645 wrote: post #2

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.

Re: Rosette – A solver-aided programming language that extends Racket

#4

Post by bandali » Sun, Jun 04, 2017, 3:43 PM UTC

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...

Re: Rosette – A solver-aided programming language that extends Racket

#5

Post by nickpsecurity » Sun, Jun 04, 2017, 4:43 PM UTC

agumonkey wrote: post #3

throwaway7645 wrote: post #2

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

Re: Rosette – A solver-aided programming language that extends Racket

#6

Post by peternicky » Sun, Jun 04, 2017, 6:07 PM UTC

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

Re: Rosette – A solver-aided programming language that extends Racket

#7

Post by DanielBMarkham » Sun, Jun 04, 2017, 6:33 PM UTC

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

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

Re: Rosette – A solver-aided programming language that extends Racket

#8

Post by notjack » Sun, Jun 04, 2017, 6:39 PM UTC

DanielBMarkham wrote: post #7

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.

Re: Rosette – A solver-aided programming language that extends Racket

#9

Post by throwaway7645 » Sun, Jun 04, 2017, 7:02 PM UTC

nickpsecurity wrote: post #5

agumonkey wrote: post #3

Earlier quoted context omitted.

Ohh you're teasing me.

Here's the tease: https://www.youtube.com/watch?v=zMfdef-nYGY

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

Re: Rosette – A solver-aided programming language that extends Racket

#10

Post by nickpsecurity » Sun, Jun 04, 2017, 7:48 PM UTC

throwaway7645 wrote: post #9

nickpsecurity wrote: post #5

Earlier quoted context omitted.

Here's the tease: https://www.youtube.com/watch?v=zMfdef-nYGY

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

The DSL is a Berkley project:

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