Toward Programming Languages for Reasoning: Humans, Symbolic Systems, and AI Agents

TL;DR

This paper advocates for a new programming language approach focused on simplifying reasoning about code and semantics, aiming to improve development, AI integration, and software democratization.

Contribution

It introduces the Bosque language and platform, proposing radical simplification to enhance reasoning and address core challenges in modern software development and AI integration.

Findings

Bosque simplifies language features to improve reasoning about code.

The approach aims to unify human, symbolic, and AI reasoning in programming.

Potential to accelerate development and democratize programming.

Abstract

Integration, composition, mechanization, and AI assisted development are the driving themes in the future of software development. At their core these concepts are rooted in the increasingly important role of computing in our world, the desire to deliver functionality faster, with higher quality, and to empower more people to benefit from programmatic automation. These themes, and how they impact the human developers driving them, are the foundations for the next generation of programming languages. At first glance the needs of mechanization tools, AI agents, and human developers along with the various goals around development velocity, software quality, and software democratization are a broad and seemingly diverse set of needs. However, at their core is a single challenge that, once resolved, enables us to make radical progress in all of these areas. Our hypothesis is that, fundamentally, software development is a problem of reasoning about code and semantics. This is true for human developers implementing a feature, symbolic tools building models of application behavior, and even for language based AI agents as they perform tasks. While the particular aspects of reasoning that each agent struggles with varies to some degree, they share many common themes and, surprisingly, most mainstream languages extensively employ (anti)features that make this task harder or infeasible! This paper proposes a novel approach to this challenge -- instead of new language features or logical constructs, that add more complexity to what is already a problem of complexity, we propose radical simplification in the form of the Bosque platform and language.