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

[ivan-gandhi.livejournal.com]

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

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

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