Principle: Flow checking

proposals/p6118.md

@@ -0,0 +1,143 @@
+# Flow checking
+
+<!--
+Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+Exceptions. See /LICENSE for license information.
+SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+-->
+
+[Pull request](https://github.com/carbon-language/carbon-lang/pull/6118)
+
+<!-- toc -->
+
+## Table of contents
+
+-   [Abstract](#abstract)
+-   [Problem](#problem)
+-   [Background](#background)
+-   [Proposal](#proposal)
+-   [Details](#details)
+-   [Rationale](#rationale)
+-   [Alternatives considered](#alternatives-considered)
+
+<!-- tocstop -->
+
+TODOs indicate where content should be updated for a proposal. See
+[Carbon Governance and Evolution](/docs/project/evolution.md) for more details.
+
+## Abstract
+
+Carbon's language goals include support for
+[practical safety mechanisms](../docs/project/goals.md#practical-safety-and-testing-mechanisms). 
+The [updated](p5914.md) Carbon safety strategy clarifies this by including
+the requirement of using Carbon as a "rigorously memory safe programming language".
+
+This proposal introduces a principle "flow checking" to clarify, at a high level,
+a technical approach to memory safety through static checking.
+
+## Problem
+
+A programming language design can support static checking in many different ways.
+Ensuring safety as a language property is inseparably tied to design choices.
+By clarifying the high-level approach taken and its commonality and difference 
+with models like Rust, we clarify the design options, identify open
+questions and enable more concrete discussion.
+
+## Background
+
+A language design that supports both temporal memory safety and fine-grained control
+over memory for performance-sensitive is a very hard problem.
+
+TODO: Is there any background that readers should consider to fully understand
+this problem and your approach to solving it?
+
+## Proposal
+
+Flow checking is a specific form of static checking that is defined by the following characteristics: 
+
+* flow- and path-sensitivity: flow checking ensures properties that hold at every program point,
+  taking into account information available from instructions and certain branch conditions leading up
+* hybrid: flow checking is layered over a core, flow-insensitive type system as a "conservative extension".
+  Code must be accepted by the type system to be considered for flow checking, and information obtained through
+  flow checking does not influence type system.
+* can optionally rely on annotations to specify effects of operations. This information can be used to identiy 
+  operations as erroneous, even if they look acceptable from a type checking point of view.
+
+This definition is intentionally abstract and leaves out constraints on the type systems. A core type
+system statically checks which operations are permitted on data. This gives possibility of enforcing
+a programming discipline that maintains global invariants, which in turn can be useful for memory
+safety and flow checking.
+
+Rust borrow checking is one form of flow checking system that relies heavily on type invariants
+("aliasing-xor-mutability"). Rust does not need effect annotations because the type invariants are 
+very strong and generic library types that provide functionality provide sound operations where
+the strength of the invariants hurt expressivity.
+
+Carbon's system of flow checking may choose less strong type invariants and/or different core 
+library operations to enable sound memory safe programming patterns. In particular, it
+is possible to come up with more permissive regime for control of aliasing and non-interference.
+
+## Details
+
+TODO: Fully explain the details of the proposed solution.
+
+Temporal memory safety is mainly about ensuring reference and pointer validity in
+the presence of operations that render them invalid.
+
+For a given memory location (place) $\pi$ and a program construct $p$ that refers to it, 
+the following core operations are a form of memory access that relies on `p` being a valid:
+
+* dereference `*p`
+* member access `p.m`
+* element access `p[i]`
+
+Carbon programs manipulate memory locations, which affects whether a given location $\pi$
+will satisfy the conditions safe access. We are often able to deduce from static properties
+like well-typedness whether program access will be safe. In general, this problem
+is undecidable, so static checking has to work with approximations.
+
+A standalone flow-insensitive type discipline that aims to provide safety has to
+satisfy the following statement (type soundness):
+
+> If (program is well-typed) then (program execution is safe)
+
+We accept that type checking restricts programmers: there are safe programs which may not pass type checking.
+Carbon's goal of incremental migration from C++ is fundamentally in conflict with such a notion
+of type soundness: idiomatic C++ code may use programming patterns that are safe to execute but
+fail to rigorous safety checks that enable compilers to verify.
+
+Thus, we pursue rigorous safety through a split into type and flow checking:
+
+> If (program is well-typed) then (if (program is flow-checked) then (program execution is safe))
+
+Type safety in languages like C++ has come to mean preventing type errors due to mismatching
+between data and supported operations. This is not enough for memory safety and sound execution.
+Carbon's permissive mode (TODO: link) must apply the same type checking algorithm to a
+programs that correspond to migrated C++ as well as Carbon programs that are rigorously memory safe.
+
+## Rationale
+
+TODO: How does this proposal effectively advance Carbon's goals? Rather than
+re-stating the full motivation, this should connect that motivation back to
+Carbon's stated goals and principles. This may evolve during review. Use links
+to appropriate sections of [`/docs/project/goals.md`](/docs/project/goals.md),
+and/or to documents in [`/docs/project/principles`](/docs/project/principles).
+For example:
+
+-   [Community and culture](/docs/project/goals.md#community-and-culture)
+-   [Language tools and ecosystem](/docs/project/goals.md#language-tools-and-ecosystem)
+-   [Performance-critical software](/docs/project/goals.md#performance-critical-software)
+-   [Software and language evolution](/docs/project/goals.md#software-and-language-evolution)
+-   [Code that is easy to read, understand, and write](/docs/project/goals.md#code-that-is-easy-to-read-understand-and-write)
+-   [Practical safety and testing mechanisms](/docs/project/goals.md#practical-safety-and-testing-mechanisms)
+-   [Fast and scalable development](/docs/project/goals.md#fast-and-scalable-development)
+-   [Modern OS platforms, hardware architectures, and environments](/docs/project/goals.md#modern-os-platforms-hardware-architectures-and-environments)
+-   [Interoperability with and migration from existing C++ code](/docs/project/goals.md#interoperability-with-and-migration-from-existing-c-code)
+
+## Alternatives considered
+
+Rust borrow checking can be considered a flow checking system that is built on strong type invariants.
+The strong type invariants make migration from C++ very difficult as they require a type discipline that
+is incompatible with many established C++ patterns.
+
+TODO: What alternative solutions have you considered?