{"id":185,"date":"2010-11-16T15:48:50","date_gmt":"2010-11-16T15:48:50","guid":{"rendered":"http:\/\/computable.cl\/blog\/?p=185"},"modified":"2010-11-16T15:48:50","modified_gmt":"2010-11-16T15:48:50","slug":"tla-menos-que-mas-lo-poco-que-nos-dijo-lamport","status":"publish","type":"post","link":"http:\/\/www.computable.cl\/blog\/?p=185","title":{"rendered":"TLA: menos que m\u00e1s, lo poco que nos dijo Lamport"},"content":{"rendered":"<p>El d\u00eda de ayer el connotado creador de\u00a0<em>LaTeX<\/em>,\u00a0<em>Leslei Lamport<\/em><em> <\/em>de paso por Chile dio una charla plenaria en el\u00a0<em>Departamento de Ciencias de la Computaci\u00f3n de la Universidad de Chile<\/em>, aclarando que este es uno de los centros de investigaci\u00f3n y departamento en el \u00e1rea m\u00e1s solventes acad\u00e9micamente en Chile y en el contexto latinoamericano. Su charla titulada \u00a8How to write a proof?\u00a8 m\u00e1s que ser una introducci\u00f3n a un nuevo\u00a0<em>paradigma<\/em>, fue un intento por\u00a0<em>seducir sin el sex-appeal<\/em><em> <\/em>y as\u00ed proponernos su enfoque materializado en su proyecto lenguaje\u00a0<em>TLA: Temporal Logic of Actions,<\/em><em> <\/em><em>que es y no es m\u00e1s<\/em> como \u00e9l mismo lo presenta un\u00a0<em>lenguaje formalizado para la especificaci\u00f3n de demostraciones<\/em>. Su presentaci\u00f3n fue un itinerario desde lo que el denomino la\u00a0<em>escritura de demostraciones<\/em> del Siglo XVII, pasando por la del siglo XX y d\u00e1ndonos los\u00a0<em>retazos formales<\/em> de su propuesta para la escritura del siglo XXI, m\u00e1s de alguien se sintio aludido a que aqu\u00ed en Chile aun hacemos las cosas como si estuviesemos en el siglo XVII. Creo que\u00a0<em>para todos<\/em> los que estuvimos all\u00ed, sentimos\u00a0 desde su\u00a0<em>rectus<\/em><em> <\/em>una no despreciable cuota de\u00a0<em>condescendencia. P<\/em>asando por el alto el tono de su discurso, \u00a0no nos queda m\u00e1s preguntarnos lo pertinente, y que para mi tiene que ver con resolver la relaci\u00f3n existente entre la propuesta de\u00a0<em>Don Leslie <\/em>y otros propuesta ya existentes, la \u00a0respuesta\u00a0<em>PhD. Lamport<\/em> fue poco alentadora y peor a\u00fan <em>displicente<\/em> al comentar que el camino recorrido por esta alternativas, me refiero con ellas a lo que hoy por hoy se conoce como el enfoque de los sistemas\u00a0<em>MetaMath<\/em> y que son los v\u00e1stagos para \u00a0esta nueva centuria que comienza de los formalismos\u00a0<em>no-clasicistas<\/em> tales como\u00a0<em>intuicionista y constructivistas<\/em> . Creo que puedo comentar que para pesar de\u00a0<em>Lamport<\/em> estas nuevas comunidades, aquellas que crecen alrededor de los a<em>sistentes de demostraciones<\/em>, o mejor dicho\u00a0<em>proof assistants,<\/em> cuentan con una\u00a0<em>serie de \u00e9xitos <\/em>importantes a su haber, que por lo que pude constatar\u00a0<em>Mr. Lamport y su TLA<\/em> no han logrado emular, entonces \u00bfPor qu\u00e9 subestimar otros enfoques? La respuesta de\u00a0<em>Lamport <\/em>fue <em>nuevamente condescendiente<\/em><em> <\/em>refiri\u00e9ndose a que estas ventajas, aquellas que poseen los enfoques basados en las\u00a0<em>l\u00f3gicas minimalistas<\/em> ser\u00e1n finalmente superadas y que estas tienen fecha de termino, que al finalizar esta centuria, aquellas ventajas tales como\u00a0<em>eficiencia computacional<\/em> ser\u00e1n alcanzadas por el\u00a0<em>enfoque cl\u00e1sico<\/em> y que este superar\u00eda en definitiva a este referente alternativo gracias a la\u00a0<em>fuerza bruta<\/em> obtenida desde las\u00a0<em>nuevas generaciones de m\u00e1quinas<\/em>. De sus comentarios s\u00f3lo puedo desprender un postura conocida y tristemente celebre entre cient\u00edficos, y esta es que mientras el\u00a0<em>m\u00fasculo de la producci\u00f3n sea tonificado<\/em> se nos permitir\u00e1 alcanzar y superar cualquiera de las metas y dificultades que se nos pongan por delante. Me temo\u00a0<em>Sr. Lamport<\/em> que la historia nos deparar\u00e1 una aventura mucho m\u00e1s entretenida y excitante de lo que usted conjetura, hemos visto como un sinf\u00edn de artefactos sofisticados pero finalmente in\u00fatiles cuelgan de las galer\u00edas de los museos.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>El d\u00eda de ayer el connotado creador de\u00a0LaTeX,\u00a0Leslei Lamport de paso por Chile dio una charla plenaria en el\u00a0Departamento de Ciencias de la Computaci\u00f3n de la Universidad de Chile, aclarando que este es uno de los centros de investigaci\u00f3n y departamento en el \u00e1rea m\u00e1s solventes acad\u00e9micamente en Chile y en el contexto latinoamericano. Su<a class=\"read-more \" href=\"http:\/\/www.computable.cl\/blog\/?p=185\" title=\"Read More\"> <span class=\"button default\">Read More<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[],"tags":[],"class_list":["post-185","post","type-post","status-publish","format-standard","hentry"],"_links":{"self":[{"href":"http:\/\/www.computable.cl\/blog\/index.php?rest_route=\/wp\/v2\/posts\/185","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.computable.cl\/blog\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.computable.cl\/blog\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.computable.cl\/blog\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.computable.cl\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=185"}],"version-history":[{"count":2,"href":"http:\/\/www.computable.cl\/blog\/index.php?rest_route=\/wp\/v2\/posts\/185\/revisions"}],"predecessor-version":[{"id":187,"href":"http:\/\/www.computable.cl\/blog\/index.php?rest_route=\/wp\/v2\/posts\/185\/revisions\/187"}],"wp:attachment":[{"href":"http:\/\/www.computable.cl\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=185"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.computable.cl\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=185"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.computable.cl\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=185"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}