A glimpse of future

[thedeemon]

Agda (from version 2.2.6) has a command, ‘Auto’, which searches for type inhabitants. It can be used as an aid when interactively constructing terms in Agda. In a system with dependent types it can be meaningful to use such a tool for finding fragments of, not only proofs, but also programs. For instance, giving the type signature of the map function over vectors, you will get the desired function as the first solution.
The tool is based on a term search implementation independent of Agda called ‘Agsy’. Agsy is a general purpose search algorithm for a dependently typed language similar to Agda. One shouldn’t expect it to handle large problems of any particular kind, but small enough problems of almost any kind.
Any solution coming from Auto is checked by Agda.
оттудова

В глаза еще не видел, но по описанию очень похоже на то, о чем я недавно говорил в посте про будущее программирования.

Comments

[gds.livejournal.com]

да ну, унылое говно ведь это. Я за неявные фишки (правда, касаемо планировщика) уже говорил, про это тем более скажу.
Понятно, что зависимые типы делают так, что в некоторых случаях оно катит, но всё же.

[nivanych.livejournal.com]

Почему это унылое? Весёлое, бодрое!
Код по спецификации так генерить, это не ерунда, всё-таки.
Те же RFC довольно чотко описывают.
Ну и есть одно применение, когда качество сгенерированного почти похер — это доказательства.