Nostralangus: Prophecy-based programming





Publicado en

Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023)

Licencia Creative Commons


In this work in progress, we explore the possibility of having a new operator capable of bringing information about the system in the future. While previous works define \emph{prophecy variables} as a way of inspecting the state of the system in the future, we propose to write programs that can actively use such information to choose what agents can do now. Verification techniques define systems where no \textbf{paradoxes} can be introduced but information from the future is still accessible to us as verifiers. In this document, we liberate the programs of such restriction equipping programs with a prophetic conditional operation: (<if> , \mathcal{P}(\Phi) , <then> , \mathcal{A} , <else> , \mathcal{B}). Actions (\mathcal{A}) and (\mathcal{B}) are executed depending on a future predicate (\Phi) about the system. Both sets of actions (\mathcal{A}) and (\mathcal{B}) can contradict the prophecy creating paradoxes. We explore how we can rule out some paradoxes appealing to different execution systems and two interpretations of prophecies. One of \emph{possible worlds} where making a prediction generates two possible worlds, one on which the prediction is true and another on which is false. Another interpretation in which the time is linearized using a try-catch interpretation.


Acerca de Ceresa, Martin

Palabras clave

Programming Languages, Specification, Verification, Prophecy Variables
Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX