[Haskell-cafe] ANN: spec2code
Greg Fitzgerald
With spec2code, developers no longer need to acknowledge the mundane
details of programming, such as memory allocation, bounds-checking,
byte ordering, inheritance models or performance tuning. spec2code
uses the latest techniques in compiler optimization to derive a
deterministic implementation from only a high-level specification.
For example, an optimal quicksort is derived from the following specification.
sort :: Ord a => [a] -> (b | ordered b)
sort = undefined
ordered :: Ord a => [a] -> Bool
ordered [] = True
ordered [_] = True
ordered (x1:x2:xs) = x2 > x1 && ordered (x2:xs)
Read as, “the function 'sort' takes a list of orderable list items,
and returns a list for which each list item is greater to the one
preceding it.”
How does it work? By telling the compiler about the logical
properties of how its output relates to its input, the compiler is
sufficiently constrained to apply its genetic algorithm. It iterates
over the specification with all known optimization techniques,
algebraically reducing the program to an underlying machine model.
The compiler uses static analysis and complexity theory in conjunction
with the machine model to order implementations by their performance
characteristics and choose the optimal one. Conceptually, the first
phase orders algorithms by complexity, using "average case", "worst
case" and "memory consumption":
[MergeSort (n*log n) (n*log n) n,
QuickSort (n*log n) (n*n) (log n),
InsertionSort (n*n) (n*n) 1,
BubbleSort (n*n) (n*n) 1
]
After choosing a high-level algorithm, spec2code does the usual
low-level optimizations via LLVM to map the algorithm to optimal
native code.
Does it scale? Absolutely, spec2code is not confined to
specifications for which optimized algorithms are already known.
spec2code can be used to implement operation systems, device drivers,
build systems, package management tools, and even do your shirt
laundry. spec2code will change your job from programmer to
specification author, giving you more time for meetings, managing
email, and browsing the web. Say goodbye to those dirty Perl scripts,
broken C code, and ultimately, your job. spec2code is the future of
programming and the beginning of the end of mankind.
Looking forward to obsoleting you soon,
Greg
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Heinrich Apfelmus
> After 5 years of R&D, I’m proud to announce the spec2code compiler.
> With spec2code, developers no longer need to acknowledge the mundane
> details of programming, such as memory allocation, bounds-checking,
> byte ordering, inheritance models or performance tuning. spec2code
> uses the latest techniques in compiler optimization to derive a
> deterministic implementation from only a high-level specification.
>
>
> Does it scale? Absolutely, spec2code is not confined to
> specifications for which optimized algorithms are already known.
> spec2code can be used to implement operation systems, device drivers,
> build systems, package management tools, and even do your shirt
> laundry. spec2code will change your job from programmer to
> specification author, giving you more time for meetings, managing
> email, and browsing the web. Say goodbye to those dirty Perl scripts,
> broken C code, and ultimately, your job. spec2code is the future of
> programming and the beginning of the end of mankind.
>
> Looking forward to obsoleting you soon,
Awesome! Given the great potential of the new spec2code compiler, the
reception seems to be somewhat chilly. But maybe that's because no one
likes to be obsoleted...
In fact, I do have to admit that I'm secretly working on a specification
of a program that halts exactly when spec2code produces a program that
does not halt. It's my only hope!
Regards,
Heinrich Apfelmus
Tom Hawkins
<apfe...@quantentunnel.de> wrote:
>> Does it scale? Absolutely, spec2code is not confined to
>> specifications for which optimized algorithms are already known.
>> spec2code can be used to implement operation systems, device drivers,
>> build systems, package management tools, and even do your shirt
>> laundry. spec2code will change your job from programmer to
>> specification author, giving you more time for meetings, managing
>> email, and browsing the web. Say goodbye to those dirty Perl scripts,
>> broken C code, and ultimately, your job. spec2code is the future of
>> programming and the beginning of the end of mankind.
>>
>> Looking forward to obsoleting you soon,
>
> Awesome! Given the great potential of the new spec2code compiler, the
> reception seems to be somewhat chilly. But maybe that's because no one
> likes to be obsoleted...
Or it could just be that time of year. (Apr 1st)
_______________________________________________
Haskell mailing list
Has...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell