From 2865366ec82babbfb74f49edf1f6bd66e69521ca Mon Sep 17 00:00:00 2001 From: Burak Emir Date: Mon, 29 Sep 2025 07:57:31 +0000 Subject: [PATCH 1/4] Add new safety principle page, following update to safety strategy. --- docs/project/principles/safety.md | 62 +++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 docs/project/principles/safety.md diff --git a/docs/project/principles/safety.md b/docs/project/principles/safety.md new file mode 100644 index 0000000000000..932b63b401893 --- /dev/null +++ b/docs/project/principles/safety.md @@ -0,0 +1,62 @@ +# Safety + + + + + +## Distinction between Strict and Permissive Carbon + +For any sufficiently expressive programming language, it is +undecidable whether the execution of programs in that language +will have interesting properties. + +Any language that aims to provides rigorous memory safety guarantees +thus needs to navigate a tension between safety and +expressivity. + +For Carbon, we distinguish between a *strict* and a *permissive* +variant of the Carbon language, which provides rigorous memory safety guarantees, +and a *permissive* variant that provides no such guarantees. + +A strict-Carbon program fragment is only accepted by the compiler +if execution is guaranteed to be free of safety-related execution errors +and its behavior with respect to safety is predictable. + +A permissive-Carbon program is accepted independent of whether it may +or may not have safety errors. In particular, a permissive-Carbon program +can call C++ code without the programmer having to give any additional +information that may be required for checking safety. + +## Partial Safety and Gradual Ramp-up + +While absence of safety-related errors is a property of a program as +a whole, the design must specify the boundary and interaction between +strict-Carbon and permissive-Carbon fragments in a way that benefits +from partial safety guarantees. + +In particular, it must be possible to turn permissive-Carbon code that +calls C++ or was migrated from C++ into safe-Carbon by gradual adoption +of safety-related annotations. + +Annotations for static checking need to be [easy to read and write](../goals.md#code-that-is-easy-to-read-understand-and-write), and program safety must +be attainable without being forced to fully rewrite migrated C++ and +without performance cost. + +Annotations may include programmer adding assumptions that enable +the compiler to apply the rules of safe-Carbon to obtain a proof of +safety. + +## Simplicity + +The rules that determine whether a safe-Carbon program is accepted +should be easy to understand and documented. + +Different build modes never change the rules that make +safe-Carbon safe (safe-Carbon is safe in any build mode), but +they may affect behavior and performance characteristics of +Carbon programs as a whole. + From 94922acd230df51af038e40b9baf5b8807227664 Mon Sep 17 00:00:00 2001 From: Burak Emir Date: Mon, 29 Sep 2025 13:44:18 +0000 Subject: [PATCH 2/4] Add index entry, and reword. --- docs/project/principles/README.md | 1 + docs/project/principles/safety.md | 61 +++++++++++++++++++------------ 2 files changed, 39 insertions(+), 23 deletions(-) diff --git a/docs/project/principles/README.md b/docs/project/principles/README.md index 173afd5f88859..da919410eda73 100644 --- a/docs/project/principles/README.md +++ b/docs/project/principles/README.md @@ -25,5 +25,6 @@ wants to pursue, as well as those we want to exclude. - [Information accumulation](information_accumulation.md) - [Low context-sensitivity](low_context_sensitivity.md) - [Prefer providing only one way to do a given thing](one_way.md) +- [Safety](safety.md) - [One static open extension mechanism](static_open_extension.md) - [Success criteria](success_criteria.md) diff --git a/docs/project/principles/safety.md b/docs/project/principles/safety.md index 932b63b401893..7068eadf74146 100644 --- a/docs/project/principles/safety.md +++ b/docs/project/principles/safety.md @@ -8,28 +8,40 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception -## Distinction between Strict and Permissive Carbon +## Static Checking For any sufficiently expressive programming language, it is undecidable whether the execution of programs in that language will have interesting properties. -Any language that aims to provides rigorous memory safety guarantees -thus needs to navigate a tension between safety and -expressivity. +*Static checking* is a compile-time method to ensure program properties through +analysis and annotations that describe intended behavior. -For Carbon, we distinguish between a *strict* and a *permissive* -variant of the Carbon language, which provides rigorous memory safety guarantees, -and a *permissive* variant that provides no such guarantees. +A language that aims to provides rigorous memory safety guarantees +through static checking needs to navigate a tension between safety and +expressivity. Carbon aims to provide a memory-safe language, which +means statically checked language that covers realistic programming +use cases. + +## Strict and Permissive Carbon + +The goals of Carbon include incremental migration from C++. Further, +interactions with system components not written in Carbon place a limit +on safety guarantees. + +For this reason, we distinguish between a *strict* and a *permissive* variant of the Carbon +language. The strict variant provides rigorous memory safety guarantees, +whereas the *permissive* variant does not provides no such guarantees. A strict-Carbon program fragment is only accepted by the compiler if execution is guaranteed to be free of safety-related execution errors and its behavior with respect to safety is predictable. -A permissive-Carbon program is accepted independent of whether it may -or may not have safety errors. In particular, a permissive-Carbon program -can call C++ code without the programmer having to give any additional -information that may be required for checking safety. +A permissive-Carbon program is accepted independent without any guarantee +whether its execution may lead to safety errors. In particular, a +permissive-Carbon program fragment can call C++ code. The +programmer does not have to give additional information to the compiler +which is necessary for checking safety. ## Partial Safety and Gradual Ramp-up @@ -38,25 +50,28 @@ a whole, the design must specify the boundary and interaction between strict-Carbon and permissive-Carbon fragments in a way that benefits from partial safety guarantees. -In particular, it must be possible to turn permissive-Carbon code that -calls C++ or was migrated from C++ into safe-Carbon by gradual adoption +A strict-Carbon program fragment may safely interact with a permissive-Carbon fragment +if the conditions for safe execution are met. + +It will be possible and necessary to *assume* such safety conditions. In permissive +code, the responsibility for safety lies with the programmer. +Carbon's safety model may support communicating part or all of the assumed +information to the compiler which can make use of it for safety checking. + +It must further be possible to turn permissive-Carbon code into safe-Carbon by gradual adoption of safety-related annotations. +## Simplicity and Ease of Understanding + Annotations for static checking need to be [easy to read and write](../goals.md#code-that-is-easy-to-read-understand-and-write), and program safety must be attainable without being forced to fully rewrite migrated C++ and without performance cost. -Annotations may include programmer adding assumptions that enable -the compiler to apply the rules of safe-Carbon to obtain a proof of -safety. - -## Simplicity - -The rules that determine whether a safe-Carbon program is accepted -should be easy to understand and documented. +The rules that determine whether a strict-Carbon program is accepted +should be documented and easy to understand. Different build modes never change the rules that make -safe-Carbon safe (safe-Carbon is safe in any build mode), but -they may affect behavior and performance characteristics of +safe-Carbon safe (safe-Carbon is safe in any build mode). +They may affect behavior and performance characteristics of Carbon programs as a whole. From a558a523592a78b311b330d8c5e17a82a7bf2b47 Mon Sep 17 00:00:00 2001 From: Burak Emir Date: Mon, 29 Sep 2025 13:53:06 +0000 Subject: [PATCH 3/4] reword --- docs/project/principles/safety.md | 24 ++++++++++++++---------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/docs/project/principles/safety.md b/docs/project/principles/safety.md index 7068eadf74146..739d79c434d76 100644 --- a/docs/project/principles/safety.md +++ b/docs/project/principles/safety.md @@ -17,24 +17,28 @@ will have interesting properties. *Static checking* is a compile-time method to ensure program properties through analysis and annotations that describe intended behavior. -A language that aims to provides rigorous memory safety guarantees -through static checking needs to navigate a tension between safety and -expressivity. Carbon aims to provide a memory-safe language, which -means statically checked language that covers realistic programming -use cases. +Carbon aims to provides rigorous memory safety guarantees +through static checking. This requires navigating a field of tension +between safety and expressivity. Carbon's statically checked safety +guarantees should not come at the price of losing possibility to cover +realistic programming use cases. + +Static checking cannot fully eliminate the need for dynamic techniques +for safety (e.g. bounds checks) but it can provide constraints on +runtime program behaviors to minimize such checks. ## Strict and Permissive Carbon -The goals of Carbon include incremental migration from C++. Further, +The goals of Carbon include incremental migration from C++, which does not +come withs statically checked safety guarantees. Further, interactions with system components not written in Carbon place a limit on safety guarantees. -For this reason, we distinguish between a *strict* and a *permissive* variant of the Carbon -language. The strict variant provides rigorous memory safety guarantees, -whereas the *permissive* variant does not provides no such guarantees. +For this reason, Carbon's design distinguishes between a *strict* and a *permissive* variant of the +language and clarifies the interaction and boundary between these variants. A strict-Carbon program fragment is only accepted by the compiler -if execution is guaranteed to be free of safety-related execution errors +if execution is guaranteed to be entirely free of safety-related execution errors and its behavior with respect to safety is predictable. A permissive-Carbon program is accepted independent without any guarantee From 5029cf15ec2737f462d8dd1261b451c2dc5550a7 Mon Sep 17 00:00:00 2001 From: Burak Emir Date: Wed, 1 Oct 2025 07:12:16 +0000 Subject: [PATCH 4/4] update, format --- docs/project/principles/safety.md | 110 +++++++++++++++++------------- 1 file changed, 61 insertions(+), 49 deletions(-) diff --git a/docs/project/principles/safety.md b/docs/project/principles/safety.md index 739d79c434d76..187ba7800b08b 100644 --- a/docs/project/principles/safety.md +++ b/docs/project/principles/safety.md @@ -8,74 +8,86 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception -## Static Checking +## Table of contents -For any sufficiently expressive programming language, it is -undecidable whether the execution of programs in that language -will have interesting properties. +- [Static Checking](#static-checking) +- [Strict and Permissive Carbon](#strict-and-permissive-carbon) +- [Partial Safety and Gradual Ramp-up](#partial-safety-and-gradual-ramp-up) +- [Simplicity and Ease of Understanding](#simplicity-and-ease-of-understanding) -*Static checking* is a compile-time method to ensure program properties through -analysis and annotations that describe intended behavior. + -Carbon aims to provides rigorous memory safety guarantees -through static checking. This requires navigating a field of tension -between safety and expressivity. Carbon's statically checked safety -guarantees should not come at the price of losing possibility to cover -realistic programming use cases. +## Static Checking -Static checking cannot fully eliminate the need for dynamic techniques -for safety (e.g. bounds checks) but it can provide constraints on -runtime program behaviors to minimize such checks. +For any sufficiently expressive programming language, it is undecidable whether +the execution of programs in that language will have interesting properties. -## Strict and Permissive Carbon +_Static checking_ is a compile-time method to ensure program properties through +analysis and annotations that describe intended behavior. -The goals of Carbon include incremental migration from C++, which does not -come withs statically checked safety guarantees. Further, -interactions with system components not written in Carbon place a limit -on safety guarantees. +Carbon aims to provides rigorous memory safety guarantees through static +checking. This requires navigating a field of tension between safety and +expressivity. Carbon's statically checked safety guarantees should not come at +the price of losing possibility to cover realistic programming use cases. -For this reason, Carbon's design distinguishes between a *strict* and a *permissive* variant of the -language and clarifies the interaction and boundary between these variants. +Static checking cannot fully eliminate the need for dynamic techniques for +safety (for example bounds checks) but it can provide constraints on runtime +program behaviors to minimize such checks. -A strict-Carbon program fragment is only accepted by the compiler -if execution is guaranteed to be entirely free of safety-related execution errors -and its behavior with respect to safety is predictable. +## Strict and Permissive Carbon -A permissive-Carbon program is accepted independent without any guarantee -whether its execution may lead to safety errors. In particular, a -permissive-Carbon program fragment can call C++ code. The -programmer does not have to give additional information to the compiler -which is necessary for checking safety. +The goals of Carbon include incremental migration from C++, which does not come +with an overall statically checked safety guarantee. Further, interactions with +system components not written in Carbon place a limit on safety guarantees. + +For this reason, Carbon's design distinguishes between a _strict_ and a +_permissive_ variant of the language and clarifies the interaction and boundary +between these variants. + +A strict-Carbon program fragment is only accepted by the compiler if execution +is guaranteed to be entirely free of safety-related execution errors and its +behavior with respect to safety is predictable. Where strict Carbon may call +operations where the compiler cannot prove ("unsafe operations"), a marker and +an alternative safety argument must be provided in some form. + +A permissive-Carbon program is accepted without an overall safety guarantee, so +its execution may lead to safety errors. Permissive Carbon should still perform +safety checks wherever possible, and signal errors. A permissive-Carbon program +fragment can call C++ code without a safety argument of any form. Where +additional information can enable safety checks, permissive Carbon can provide +ways to perform such check and thus obtain partial (weak) safety. Crucially, the +programmer is not obliged to give additional information to the compiler which +would be necessary for checking partial safety. ## Partial Safety and Gradual Ramp-up -While absence of safety-related errors is a property of a program as -a whole, the design must specify the boundary and interaction between -strict-Carbon and permissive-Carbon fragments in a way that benefits -from partial safety guarantees. +While absence of safety-related errors is a property of a program as a whole, +the design must specify the boundary and interaction between strict-Carbon and +permissive-Carbon fragments in a way that benefits from partial safety +guarantees. -A strict-Carbon program fragment may safely interact with a permissive-Carbon fragment -if the conditions for safe execution are met. +A strict-Carbon program fragment may safely interact with a permissive-Carbon +fragment if the conditions for safe execution are met. -It will be possible and necessary to *assume* such safety conditions. In permissive -code, the responsibility for safety lies with the programmer. +It will be possible and necessary to _assume_ such safety conditions. In +permissive code, the responsibility for safety lies with the programmer. Carbon's safety model may support communicating part or all of the assumed information to the compiler which can make use of it for safety checking. -It must further be possible to turn permissive-Carbon code into safe-Carbon by gradual adoption -of safety-related annotations. +It must further be possible to migrate permissive-Carbon code into strict-Carbon +by gradual adoption of safety-related annotations, until it is fully annotated +and benefits from statically checked overall safety guarantee of strict Carbon. ## Simplicity and Ease of Understanding -Annotations for static checking need to be [easy to read and write](../goals.md#code-that-is-easy-to-read-understand-and-write), and program safety must -be attainable without being forced to fully rewrite migrated C++ and -without performance cost. - -The rules that determine whether a strict-Carbon program is accepted -should be documented and easy to understand. +Annotations for static checking need to be +[easy to read and write](../goals.md#code-that-is-easy-to-read-understand-and-write), +and program safety must be attainable without being forced to fully rewrite +migrated C++ and without performance cost. -Different build modes never change the rules that make -safe-Carbon safe (safe-Carbon is safe in any build mode). -They may affect behavior and performance characteristics of -Carbon programs as a whole. +The rules that determine whether a strict-Carbon program is accepted should be +documented and easy to understand. +Different build modes never change the rules that make safe-Carbon safe +(safe-Carbon is safe in any build mode). They may affect behavior and +performance characteristics of Carbon programs as a whole.