This is seriously impressive stuff. "Solver-aided programming language" might sound esoteric, but it's the natural evolution of the same trend towards higher-level, more declarative programming that replaced 'goto' with 'for', and 'for' with 'map'. You can judge the merit of programming approach by how much it punches above its weight, and the list of applications written in Rosette is short but impressive[1] (especially considering it was only released in 2013). I'm particularly impressed by Chlorophyll, a "synthesis-aided programming model and compiler for GreenArrays GA144, a minimalist low-power spatial architecture":<p>>We used Chlorophyll to compile an accelerometer-based hand-gesture recognition application for GA144. This application occupied 83 nodes out of 144 nodes. In this demo, GA144 was running on 1.8 V, and the application drew 0.24 mA. This means we should be able to run this application using two lemons![2]<p>If you've never heard of the GA144, it's an amazing chip designed by Chuck Moore (inventor of Forth) that provides computational grunt comparable to an i7 for a few milliwatts, on a 180nm process no less, at the cost of an awkward architecture of a 12x12 array of chips with very little RAM whose machine language is Forth. Because of this architecture, and despite considerable interest, few have actually managed to program the GA144 to do anything interesting. This demo of an application written in Rosette might just be the most interesting thing anyone's ever gotten a GA144 to do. On that basis <i>alone</i>, I'd say they were on to something.<p>Aside: imagine a "demoscene" of who could run the most advanced application on a lemon!<p>[1] <a href="http://emina.github.io/rosette/apps.html" rel="nofollow">http://emina.github.io/rosette/apps.html</a>
[2] <a href="http://pl.eecs.berkeley.edu/projects/chlorophyll/" rel="nofollow">http://pl.eecs.berkeley.edu/projects/chlorophyll/</a>
Exactly. Why would I write a custom, small, incomplete and much slower solver by myself for my compiler, when I can just use a fast SAT solver (cryptominisat and friends), which are complete and have an acceptable license.<p>Looking at scala, pony, haskell, but really any modern language working on dependent types: python, php, cperl, ruby, ...
Interesting, but I wanted to read an easier example. For example see: <a href="http://emina.github.io/rosette/doc/rosette-guide/ch_essentials.html#%28part._sec~3aqueries%29" rel="nofollow">http://emina.github.io/rosette/doc/rosette-guide/ch_essentia...</a>
Something very similar for Haskell, as a library: <a href="http://leventerkok.github.io/sbv/" rel="nofollow">http://leventerkok.github.io/sbv/</a>