Cómo terminé coescribiendo ese artículo con Leslie Lamport
I came to write THAT paper with Leslie Lamport
Lawrence Paulson relata cómo pasó de rechazar el artículo de Leslie Lamport contra los tipos en lenguajes de especificación a coescribirlo con él. El editor Andrew Appel sugirió que Paulson y David McAllester se unieran a Lamport para hacerlo técnicamente preciso. Tras un segundo rechazo en la revisión, el artículo se publicó con una nota aclaratoria. Paulson reflexiona que, 27 años después, los sistemas de tipos han demostrado su valor en verificación, mientras que los formalismos sin tipos tienen problemas prácticos.
Sin tipos no tienes sobrecarga de notación, que es trivial en principio (puedes usar muchos símbolos distintos), pero un gran problema en la práctica.
- joomy
De alguna manera, la versión final del artículo no está enlazada desde la publicación del blog: https://www.microsoft.com/en-us/research/publication/specifi...
- srean
> El otro revisor, David McAllester, llegó al mismo veredicto.
¿El mismo David McAllester que introdujo los límites PAC-Bayesianos?
Respuesta: Sí.
- mrkeen
> Había algo de sentido en esta tesis. Los sistemas de tipos estaban en un estado de cambio en 1992 cuando se escribió esa nota. Coq (ahora Rocq) acababa de aparecer, y estaban ocurriendo grandes cambios en la teoría de tipos de Martin-Löf. En cuanto a las teorías de tipos simples, las primeras implementaciones de HOL llevaban solo un par de años. No estaba claro qué podía hacer cualquier cálculo tipado. Los asistentes de pruebas aún no soportaban clases de tipos. John Harrison estaba a años de distancia de introducir su truco para obtener tipos dependientes de bajo costo, que funcionan lo suficientemente bien para expresar Tn.
No quiero meter tipos lineales o dependientes en TLA+. Probar propiedades dinámicas con un runtime exhaustivo es un juego totalmente diferente de lo que podrías hacer estáticamente.
Pero sí quiero descartar tonterías. Claro, puedo probar que el semáforo nunca es igual a RED_LIGHT. Lástima si es igual a RED.