Рет қаралды 80
Bosque: A Development Stack for Mechanized Software Construction
Abstract: The future of software development is centered around integration, composition, automation, and AI assisted development. Bosque is a novel programming language and development stack that is designed explicitly to support this future. This is done, not via the introduction of new language constructs, but by the application of simplification and careful selection of language features to eliminate hidden semantic context and support automated reasoning. The resulting core intermediate representation (IR) is highly amenable to building automated analysis and processing tooling - sidestepping long standing problems with inductive invariants, frame-rules, and non-determinism. The surface language connects this IR to a set of simple programming language features that are familiar to modern developers and provides them with a range of simple constructs for quickly building high-quality software. This empowers users of the language, both human and AI powered, with a range of powerful tooling capabilities and enables them to confidently write, review, and process code without concern for subtle what-ifs and hidden pitfalls. This talk presents an overview of the thinking that drives the development of the Bosque development stack, covers the languages features themselves, and shows how these features combine to create new vision for software construction.