Agda. The language of the distant but imminent future.

[juan_gandhi]

Larry Diehl's yesterday slides

So, the language where type-dependence reaches the ultimate, where intuitionistic logic is just another way to express things. It was absolutely amazing.

Comments

[sorhed.livejournal.com]

Я, напротив, полагаю, что каждый успешный программист должен хоть один раз в жизни придумать собственный язык программирования. :)

[itman.livejournal.com]

Да конечно. У нас тут в прошлом году ушел успешный программист. Оставил нам свой язык программирования для реализации схем трансляции запроса. Радуемся мы этому языку практически беспрестанно!

[http://users.livejournal.com/_windwalker_/]

я когда-то аналог JSON-а придумал. Для хранения состояния объектов на форме. Чисто client side, безо всяких там JSP или ASP.

[ivan-gandhi.livejournal.com]

А если объекты в качестве ключей в хешах использовать, разве не то ж выходит? (пардон, надо бы попробовать)

[http://users.livejournal.com/_windwalker_/]

ну в общем да. я там в куку состояние сохранял, а потом из неё путём матов и eval пытался достать.

[ivan-gandhi.livejournal.com]

С кукой два фактора. Во-первых, надо утрамбовывать (в Гугле за куками лично Мариса следит; мне разрешили шесть байт); во-вторых, учитывать, что структура контента может меняться, при этом надо сохранять совместимость.

[http://users.livejournal.com/_windwalker_/]

ну у нас было всё проще - кровавый оффшор, где отдельные сеньёры генерят "уникальные значения" путём склеивания 4-х рандомов. И когда в какой-то момент максимальное количество разрёшённых кук было превышено, то ведущий программист сделал удивлённый хлопок глазками - а, что есть лимит ?