A logical framework to model software development by multiple agents following a common specification

TL;DR

This paper introduces a logical framework for modeling multi-agent software development from a common specification, focusing on translation between different programming settings and ensuring reliable correspondence of generated programs.

Contribution

It extends a logical framework to reason about programs, their iterative development, and translations, providing formal guarantees of translation reliability between different program generators.

Findings

Defined a notion of translation between program outputs

Proved reliable translation exists when generators follow the same specification

Extended the framework to include reasoning about iterative program development

Abstract

In this paper, we address program development by multiple different programmers (or programming teams), each working in different settings (programming languages or reasoning frameworks), but following a common specification; in particular, we examine at an abstract level the problem of translatability between their produced programs. To this end, after consideration of some philosophical issues regarding program development, including its similarities and dissimilarities with scientific theorising, we extend a logical framework built to describe scientific theorising in relativist settings: our extensions add the ability of reasoning about programs, the iterative process of their generation, and their specifications. We are thus able to define a notion of translation between the outputs of program generators and prove that there is a (trivial) such translation when two program generators follow the same specification reliably (in a specific sense of reliability).