Adds extracted principles that are underlying Carbon safety #6142
Conversation
github-actions
bot
added
the
documentation
docs/project/principles/safety.md
Outdated
| 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 |
There was a problem hiding this comment.
Should set up pre-commit according to https://github.com/carbon-language/carbon-lang/blob/trunk/docs/project/contribution_tools.md to get auto-formatting.
docs/project/principles/safety.md
Outdated
| ## Strict and Permissive Carbon | ||
|
|
||
| The goals of Carbon include incremental migration from C++, which does not | ||
| come withs statically checked safety guarantees. Further, |
There was a problem hiding this comment.
| come withs statically checked safety guarantees. Further, | |
| come with as many statically checked safety guarantees. Further, |
There was a problem hiding this comment.
I think this is a recurring source of misunderstanding where I may need to adapt my writing. I see "safety" as a global property (like "type soundness"), a language either has it or not, whereas your suggestion indicates that there may be multiple different safety guarantees.
I believe words like "rigorous memory safety" and "memory-safe language" suggests an overall guarantee that all memory-safety bugs are prevented. C++ does not come with any guarantee here, actually, does it help if I change to singular?
docs/project/principles/safety.md
Outdated
| 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. |
There was a problem hiding this comment.
Except to the extent that it performs (explicitly marked) unsafe operations, including things like calls to C++ code.
There was a problem hiding this comment.
The next section "partial safety" goes into this.
I have added a sentence saying that a safety argument must be provided in some form when an unsafe op is performed.
docs/project/principles/safety.md
Outdated
| 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. |
There was a problem hiding this comment.
I don't think this is an accurate characterization of our plans. I think that there are limits to the checking that will be possible, dependent on the extent of safety annotations in the code and use of unsafe operations, but there is an expectation that permissive-Carbon will not disregard safety considerations entirely. My expectation is that it will be safer than C++, particularly by default, and some dangerous constructs will only be available with explicit unsafe markings.
There was a problem hiding this comment.
Reworded, but I believe there is a difference between permissive and strict Carbon? I though it was very specific that permissive Carbon can be without any markings.
I did clarify that permissive Carbon may support adding markings and thus getting to "partial" safety, avoid some bugs.
docs/project/principles/safety.md
Outdated
| 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 |
There was a problem hiding this comment.
The word assume here is too strong. The expectation is that optimizations will not be performed based only on those assumptions, and it generally won't be undefined behavior if those safety conditions are dynamically violated.
There was a problem hiding this comment.
Can you clarify what you mean? Imagine we have strict Carbon program that calls permissive Carbon function foo(p) with a pointer argument and foo will have some effects on memory, but lack effect and type annotations and such.
So we mark it as "unsafe" and we simply state the effect, so that the program fragment makes sense in strict Carbon. This statement is an "assumption of safety conditions" that I mean here, it cannot be provided or proven by the compiler.
I do not follow what you are saying. If we could guarantee absence of undefined behavior in permissive Carbon, then this is already a perfectly memory-safe language and we wouldn't have a need for strict Carbon anymore. Even reading memory by dereferencing a single pointer is an unsafe operation that can provoke undefined behavior (we don't know what the read returns and what the program will do afterwards), and we won't be willing to pay the overhead for runtime-instrumentation of every read.
docs/project/principles/safety.md
Outdated
| 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 |
There was a problem hiding this comment.
There is a switch here from strict-Carbon to safe-Carbon that I think is an inconsistency, but it could just be a gap in the explanation:
We could say safe-Carbon is a subset of both strict-Carbon and permissive-Carbon, the subset that only uses safe constructs. The difference between strict-Carbon and permissive-Carbon has more to do with whether unsafe constructs are marked, and whether safety annotations are required.
There was a problem hiding this comment.
I just mixed up strict and safe, but my understanding is that strict Carbon is supposed to be that rigorously memory safe language variant.
These are the safety principles I extracted from docs/project/principles/safety_strategy.md page.
This outdated file was supposed to be deleted #5914 and its actual deletion is part of #6013.
In the context of that PR, Josh suggested we may want keep some safety principles, which are at a higher level that safety design
This is not a proposal.
It is (my understanding of) the principles underlying the updated safety strategy.
The safety design introduced in #5914 goes into more detail.
If I have read too much into the udpated safety strategy and design, or something is missing that shouldn't be missing, please let me know.