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

[itman.livejournal.com]

It vaguely resembles APL.

[ivan-gandhi.livejournal.com]

It is pure intuitionistic logic. Pretty readable, too. I saw it first time.

[sorhed.livejournal.com]

If you want some APL, try J or K or Q. :)

[itman.livejournal.com]

a,b,c,d,e,f,g
h,i,j,k,l,m,n,o,p
q,r,s,t,u,v,w
x,y,z,
it is a real programming spree!
Люди, придумывающие новые языки программирования, должны умереть в страшных муках! :-)

[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-х рандомов. И когда в какой-то момент максимальное количество разрёшённых кук было превышено, то ведущий программист сделал удивлённый хлопок глазками - а, что есть лимит ?

[antilamer.livejournal.com]

Quite a pity that the slides don't show any reasonably complex proofs, only trivial things.

Have you looked at Coq (http://coq.inria.fr)? It's in the same direction but more complex/advanced (or complicated, if you like). They proved the 4 color theorem with it.