19 noticias
En un ensayo técnico con tono divulgativo, el autor parte de la cita "simple is not small" para distinguir dos conceptos que suelen confundirse en el diseño de software: lo pequeño (poco código, pocas piezas) y lo simple (poco acoplado, una sola "trenza"). Tomando como referencia la charla "Simple M
Bluefin se presenta principalmente como un sistema de capacidades y, en segundo lugar, como un sistema de efectos para Haskell. Esta librería, publicada por primera vez a principios de 2024, se inspira en effectful de Andrzej Rybczak y funciona como una envoltura ligera sobre el tipo IO de Haskell.
Las typeclasses (Haskell) y los traits (Rust) son mecanismos de sobrecarga que permiten resolver una llamada a método en función de los tipos de sus argumentos. Esta resolución descansa sobre una propiedad esencial: la coherencia. Un sistema de tipos es coherente cuando, para cualquier restricción g
Simon Peyton Jones, cocreador del lenguaje de programación Haskell y figura clave de la investigación en lenguajes funcionales, protagoniza una entrevista extensa en el pódcast The Peterman Pod, conducido por Ryan Peterman. La conversación, de casi hora y media, recorre la filosofía de la programaci
Evan Czaplicki, creador de Elm, presenta Acadia, una herramienta que traslada a SQL los beneficios de los lenguajes con tipos precisos como Elm, Rust o Haskell. El proyecto surge de años de frustración con la desconexión entre los tipos definidos en la base de datos y los del código de cliente y ser
Este ensayo, escrito como complemento de un texto anterior titulado 'Type Theory Weary', cuestiona la necesidad de tratar los tipos como un constructo especial dentro de la informática y la lógica. El autor sostiene que los sistemas de tipos surgieron históricamente para resolver problemas que en su
Choral es un lenguaje de programación orientado a objetos diseñado para especificar coreografías, es decir, protocolos multiparte que definen cómo varios roles (los clásicos Alice, Bob, Carol…) deben coordinarse para llevar a cabo una tarea conjunta. Su objetivo es simplificar la construcción de sis
Los métodos formales —herramientas matemáticas para especificar y verificar software— apenas se utilizan fuera de nichos académicos y de alta seguridad. Un análisis extenso repasa las razones históricas y estructurales de esta baja adopción y propone una mirada más matizada que los tópicos habituale
Este artículo adapta la charla del autor en RustConf 2024 y gira en torno a un caso de estudio singular: Netstack3, la pila de red de próxima generación de Fuchsia, escrita íntegramente en Rust y diseñada para sustituir a Netstack2, implementada en Go. El proyecto, iniciado hace seis años y desarrol
Eat Your Greens (EYG) es un lenguaje de programación funcional y tipado estáticamente cuyo objetivo declarado es servir a los creadores aficionados, no a los desarrolladores profesionales. Su autor, un ingeniero que lo concibió mientras esperaba un visado para Suecia, parte de una observación: mucha
El ingeniero Joshua Barretto propone en un ensayo que el lenguaje humano funciona como un espacio latente de alta entropía: una herramienta tecnológicamente moldeada durante milenios que facilita el razonamiento conceptual, del mismo modo que un sistema de tipos fuerte en lenguajes como Rust o Haske
Este artículo analiza los sistemas de tipos enteros en los lenguajes de programación más extendidos y defiende el enfoque de Rust como modelo más riguroso. El autor repasa cómo C, C#, Go y Swift manejan los enteros: en C, el desbordamiento de enteros con signo es comportamiento indefinido y conviven
La corrección estructural es un enfoque que modela un dominio como un grafo de nodos y aristas tipadas, donde la estructura que describe el sistema es el propio sistema. Sistemas de tipos, herramientas de construcción como Bazel, lenguajes de descripción de interfaces y bases de datos con claves for
Counterexamples in Type Systems es una obra de referencia compilada por Stephen Dolan —con colaboraciones reconocidas de Andrej Bauer, Leo White y Jeremy Yallop— que reúne treinta y un contraejemplos cuidadosamente seleccionados para ilustrar los puntos delicados, las trampas y las excepciones de lo
Neel Krishnaswami y Jeremy Yallop, de la Universidad de Cambridge, presentan en PLDI '19 (Phoenix, 22–26 de junio de 2019) un trabajo que reconcilia dos tradiciones de la construcción de analizadores sintácticos: los generadores de parsers —basados en gramáticas BNF y autómatas, con análisis en tiem
Prism es un compilador funcional de prueba de concepto desarrollado por Stephen Diehl durante los últimos tres años. Su propuesta central consiste en modelar los efectos computacionales —mutación, excepciones, generadores, entrada/salida— dentro del sistema de tipos, de modo que el programador decla
Jane Street, una de las firmas de trading cuantitativo más influyentes de Wall Street, ha anunciado la creación de un equipo dedicado a métodos formales de verificación de software, en un giro estratégico motivado por el auge de la programación agéntica. La decisión marca un cambio radical en la pos
El artículo presenta una implementación práctica en Haskell del concepto matemático de 'equipamiento profunctor' (profunctor equipment), una estructura proveniente de la teoría de categorías Higher Order Topos Theory. El autor, Bartosz Milewski, decide usar Haskell como 'juguete' para verificar comp
Este artículo aborda una pregunta común entre los desarrolladores de lenguajes de programación: ¿deberían usar un sistema de tipos Hindley-Milner (HM) o Bidireccional (Bidir)? La respuesta, según el autor, no es tan simple como elegir entre dos opciones mutuamente excluyentes. La verdadera pregunta
