A glimpse of future

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.
оттудова

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

Traffic

На днях столкнулся с оживленным движением на дороге:



( +2 )