<p>In a language like C, many functions and operators have some preconditions to work. Violating a precondition is undefined behavior. For example, when indexing an array the index must be less than the length of the array. The compiler doesn't check this, it is up to the programmer.</p>
<p>In Rust, most functions always have defined behavior. Some functions are unsafe and require specific preconditions. Violating these preconditions results in undefined behavior. For example the <a href="https://doc.rust-lang.org/std/boxed/struct.Box.html#method.from_raw" rel="noreferrer"><code>Box::from_raw</code></a> method states &quot;For this to be safe, the memory must have been allocated in accordance with the memory layout used by Box.&quot;</p>
<p>However, this is still not an ideal situation. Each unsafe method has it's own unique set of required conditions to work properly. People often use unsafe just assuming what a function will do, but without carefully reading the documentation you can easily introduce undefined behavior.</p>
<p>Another issue is, suppose a unsafe function adds a precondition, there is no way to indicate this and check for it. For example, consider a hypothetical function that operates on pointers. It used to have some special case for null pointers but this is later deprecated and removed. Since the method is already unsafe existing code will still compile normally, just potentially fail in unexpected ways when used.</p>
<h2>My question</h2>
<p>I'm wondering if there is any more comprehensive safety system, that allows explicitly specifying pre-conditions in some structural way, then force users of the function to somehow acknowledge that they are aware of the requirements to run the code safely, in such a way that the code will break if a pre-condition is added which is not acknowledged.</p>
<p>An example of something I was thinking:</p>
<pre><code>function dereference(pointer p)
    requires that p is not null
    requires that p is aligned
{
    ...
}

pointer p = get_pointer_from_somewhere()
I promise p is aligned
I promise p is not null
dereference(p)
</code></pre>
<p>Or something like this:</p>
<pre><code>function mutate_object(object o)
  requires the object is not mutated in a different thread for the duration of this function {
    ...
}
</code></pre>
<p>I'm looking for prior art on the matter. Any languages that have something like this?</p>

<undefined-behavior>
Are there languages that implement a more granular precondition system than just safe/unsafe
CC BY-SA 4.0
2023-12-02T22:24:34.613Z
My experience with Ada/SPARK preconditions was that I couldn't figure a way not to check them in productive code. Can't tell if that's what you are after here. For me, this was completely useless as most preconditions on "unsafe" code require expensive checks and some scaffolding that one would like to throw away in productive uses.
feldentm
CC BY-SA 4.0
2023-12-02T22:31:49.427Z
Another direction would be JML+Java. There, again, you'll eventually run into the issue that you need phantom memory to keep track of the status behind stuff that you are observing even if you do a formal proof. Also, proof systems make strange assumptions like memory never getting reused because it would break their assumptions on typing.
feldentm
CC BY-SA 4.0
2023-12-03T01:26:23.333Z
Take a look at Common Lisp's [Error Terminology](https://www.lispworks.com/documentation/lw61/CLHS/Body/01_db.htm) section.
Barmar
CC BY-SA 4.0
2023-12-03T03:07:06.127Z
Do refinement types count?
Seggan
CC BY-SA 4.0
2023-12-03T07:39:48.567Z
@Seggan No, those can be automatically checked by the compiler.
mousetail 'he-him'
CC BY-SA 4.0
2023-12-03T21:39:51.470Z
@mousetail Do you only want things that are not checked by the compiler? Also, when you say "can" be checked by the compiler, that probably includes quite a few things. "Cannot be checked by the compiler" (rather than "*is not* checked by the compiler) seems like a complex, and somewhat situation-dependent, requirement to me. Is that what you're looking for, though?
David Young
CC BY-SA 4.0
2023-12-05T03:20:47.820Z
@mousetail I find your example somewhat specious, because being aligned and being non-null are things that can be modelled without much difficulty by a  traditional type system; can you expand on it?  That said, you may be interested in [design by contract](https://en.wikipedia.org/wiki/Design_by_contract) and [capabilities](https://en.wikipedia.org/wiki/Object-capability_model).
Moonchild
<h2><a href="https://en.wikipedia.org/wiki/Eiffel_(programming_language)" rel="nofollow noreferrer">Eiffel</a></h2>
<p>Eiffel is an object-oriented language in which functions and methods may have preconditions, specified using the <code>require</code> keyword:</p>
<pre><code>my_list.do_all (agent (s: STRING)
     require
         not_void: s /= Void
     do
         s.append_character (',')
     ensure
         appended: s.count = old s.count + 1
     end)
</code></pre>
<p>As far as I know, Eiffel doesn't expose low-level details such as pointer alignment. However, it supports <a href="https://en.wikipedia.org/wiki/Design_by_contract" rel="nofollow noreferrer">design by contract</a> for higher-level preconditions such as that a reference is non-null (&quot;not void&quot; in Eiffel's terminology) or that a list is non-empty.</p>
<p>More details about Eiffel's design-by-contract features are given in the paper <a href="https://www.eiffel.org/doc-file/eiffel/void-safe-eiffel.pdf" rel="nofollow noreferrer"><em>Avoid a Void: The eradication of null dereferencing</em></a> by Meyer, Kogtenov &amp; Stapf. In particular, the precondition can either be statically checked, or it can be asserted (with an exception thrown at runtime if the assertion fails). Assertions must be explicit at the call-site. However, assertions can be disabled at runtime, in which case they are the more granular &quot;unsafe&quot; labels you suggested</p>
<h2><a href="https://en.wikipedia.org/wiki/Java_Modeling_Language" rel="nofollow noreferrer">Java Modelling Language (JML)</a></h2>
<p>JML is a language used to specify properties of Java programs, such that the specifications can be checked by tools such as <a href="https://www.openjml.org/" rel="nofollow noreferrer">OpenJML</a> or <a href="https://www.key-project.org/" rel="nofollow noreferrer">KeY</a>. Preconditions can be written in comments; for example, here's <a href="http://www.openjml.org/examples/binary-search.html" rel="nofollow noreferrer">binary search</a>:</p>
<pre class="lang-java prettyprint-override"><code>//@ requires sortedArray != null &amp;&amp; 0 &lt; sortedArray.length &lt; Integer.MAX_VALUE;
//@ requires \forall int i; 0 &lt;= i &lt; sortedArray.length; \forall int j; i &lt; j &lt; sortedArray.length; sortedArray[i] &lt;= sortedArray[j];
//@ old boolean containsValue = (\exists int i; 0 &lt;= i &lt; sortedArray.length; sortedArray[i] == value);
//@ ensures containsValue &lt;==&gt; 0 &lt;= \result &lt; sortedArray.length;
//@ ensures !containsValue &lt;==&gt; \result == -1;
//@ pure
public static int search(int[] sortedArray, int value) {
    // ...
}
</code></pre>
<p>The first two lines, annotated <code>//@ requires</code>, are the preconditions: in this example, that the array is non-null and non-empty, and that the array elements are in ascending order.</p>
<p>Like Eiffel, these preconditions will be checked for each call-site, and preconditions which can't be proven statically can still be asserted using <code>assert</code> statements. Like Eiffel, Java has the option to disable assertions at runtime.</p>

CC BY-SA 4.0
2023-12-02T23:00:46.733Z
2023-12-04T20:01:36.210Z
2023-12-04T20:01:36.210Z
kaya3
<p>Your example is already pretty much C++</p>
<pre><code>void dereference(T&amp; p)
    // requires that p is not null
    // requires that p is aligned
{
    std::cout &lt;&lt; p;
}

void* pv = get_pointer_from_somewhere()
T* pt = reinterpret_cast&lt;T*&gt;(pv); // I promise p is aligned, and points to a T
T&amp; rt = *pt; // I promise p is not null
dereference(rt);
</code></pre>
<p>As usual, breaking a promise leads to Undefined Behavior.</p>
<p>This is an example where C++ just happens to encode the example preconditions in the existing type system. But C++ has a Turing-complete <code>concept</code> system that allows library writes to introduce new named concepts. See for instance <a href="https://stackoverflow.com/questions/71021512/c20-concepts-how-do-i-use-concepts-to-check-if-an-object-can-use-shared-from">this StackOverflow question</a> which introduces a <code>CanMakeSharedFromThis</code> concept to check if a type supports a kind of <em>smart pointers</em>.</p>

CC BY-SA 4.0
2023-12-04T14:18:31.910Z
2023-12-04T14:18:31.910Z
MSalters
<p>Any language with monads and pattern matching (Haskell) can achieve this.  A function with type <code>Maybe a</code> can explicitly pattern pre-condition failures and returning <code>Nothing</code> instead of <code>Just a</code>. Because code using the resulting Maybe has to extract the resulting Nothing or a it's required to acknowledge the Nothing post-condition.</p>
<p>Likewise Rust has <code>Option&lt;T&gt;</code>, but I'm not familiar enough with Rust to know if Option is escapable.</p>

CC BY-SA 4.0
2023-12-04T07:47:07.173Z
2023-12-04T07:47:07.173Z
DanielN
CC BY-SA 4.0
2023-12-04T13:24:45.230Z
In these cases it is impossible to tell if the condition has been met, it's undefined behavior. Returning `None` would make the behavior defined. Which is better of course but not always possible
mousetail 'he-him'
CC BY-SA 4.0
2023-12-04T16:19:48.767Z
@mousetail Hmm, maybe I misunderstand something but aren't both of the examples in the question checkable (at runtime)? Alignment is a bit trickier since it's architecture dependent, but if you can figure out what the architecture wants addresses aligned to then you can just do a divisibility check. The non-null condition is definitely checkable.
David Young
CC BY-SA 4.0
2023-12-04T17:32:24.213Z
@DavidYoung It's more about not wanting to check at runtime (due to performance cost or it just being unnecessary) than being unable to. However, I want to use this also for conditions that are actually impossible to check at runtime.
mousetail 'he-him'
CC BY-SA 4.0
2023-12-04T18:07:52.800Z
@mousetail I think the point is really that preconditions can be expressed in the language's type system, rather than having a separate system for them. For cases where the precondition is not feasible to prove and you don't want a check at runtime, then Rust's `unwrap_unchecked()` (e.g. on an Option) gives the desired result: no runtime cost, and the code 'documenting' the assertion appears in the relevant place.
kaya3
CC BY-SA 4.0
2023-12-04T19:45:08.800Z
@mousetail You can do a lot with type system features. For example, Haskell has a feature called `newtype`. It's a zero-cost wrapper around a type (the wrapper only exists at compile time). The type checker considers it distinct from the original type. One simple usage is to define a `NotNull` type, which can never be set to null (say, created by `malloc`, you can only add non-negative integers to it, you can assign a `NotNull` to a `NotNull`, etc). You can do more complex things too, like ensuring a list is sorted before being merged. See [this](https://kataskeue.com/gdp.pdf)
David Young
CC BY-SA 4.0
2023-12-04T19:47:13.053Z
And if you really want to crash rather than having a check, it's best to crash early. So, instead of having something like a function `fn` that takes a pointer that must be non-null and crashes (or UB) otherwise, have `fn` take a `NotNull` and provide an unsafe way to make a `NotNull` (ideally that crashes right away if it's null), ideally only used at the highest level. This can be zero-cost. Even better, if you can stand the slight performance reduction, don't make it crash or give UB at all and just handle the null pointer case at the highest level in the code and provide a safe interface.
David Young
CC BY-SA 4.0
2023-12-05T00:10:50.993Z
@mousetail by it's nature you can not detect undefined behavior.  What happens is *undefined*.  Including overriding any possible check, or acting in completely unpredictable ways.

What you want, "not wanting to check at runtime" is not possible.  There is no free lunch to be had here.  If the code has dynamic values at runtime then it requires dynamic checks of those values to see if they're within precondition bounds.
DanielN
CC BY-SA 4.0
2023-12-05T09:10:14.387Z
@DanielN I don't want to detect undefined behavior. I just want some explicit way for programmers to be able to explain how they have met the conditions to avoid undefined behavior, when the compiler can't check it. And make sure the code breaks when the conditions change
mousetail 'he-him'
<p>There are languages that support something very close to this. Consider Idris 2, for example.</p>
<h1>How to write preconditions</h1>
<p>You can represent preconditions as arguments. So, for example, if you have a function that takes a natural number and returns a natural number, but it requires its argument to be non-zero you could give it the type signature:</p>
<pre><code>fn :
  (n : Nat) -&gt;
  Not (n = 0) -&gt;
  Nat
fn n proofNIsNonZero = ...
</code></pre>
<p>Since this &quot;precondition&quot; is just a regular argument, you can also pass this to other functions that require a non-negative natural number.</p>
<h1>Easily conjuring fake proofs</h1>
<p>Now, returning to the question. Idris 2 provides a feature that will unsafely convert a value of any type into a value of any other type. This &quot;function&quot; is called <code>believe_me</code>. We can use this to make a function called <code>trustMe</code>. This function will take a type and (unsafely) give back a value of that type. This can be used to conjure fake &quot;proofs&quot; of any proposition we want.</p>
<p>For more detail on how <code>believe_me</code> works in Idris, see <a href="https://docs.idris-lang.org/en/latest/tutorial/provisional.html" rel="nofollow noreferrer">this part of the documentation</a>. I believe this is for Idris 1, but I don't think this has changed much between versions.</p>
<p>Here is an example of how you might do this. Note that, to use <code>trustMe</code>, you must generally spell out the proposition that you're &quot;conjuring.&quot; I think this is what you're asking for in your question.</p>
<pre><code>trustMe : (a : Type) -&gt; a
trustMe _ = believe_me ()  -- We just use believe_me to convert the value of the Unit type into whatever type we need

data MyPtr : Type -&gt; Type where
  MkMyPtr : Nat -&gt; MyPtr a

notNull : MyPtr a -&gt; Type
notNull (MkMyPtr x) = Not (x = 0)

-- This is just used in an example definition for @aligned@
-- so it's not necessary to understand this
data Even : Nat -&gt; Type where
  EvenZ : Even 0                   -- 0 is even
  EvenS : Even x -&gt; Even (S (S x)) -- If x is even, then x + 2 is even

-- Example definition: checks if the number is even
aligned : MyPtr a -&gt; Type
aligned (MkMyPtr x) = Even x

dereference :
  (ptr : MyPtr a) -&gt;
  notNull ptr -&gt;
  aligned ptr -&gt;
  a
dereference ptr notNullProof alignedProof = ?hole1

example : MyPtr a -&gt; a
example ptr =
  dereference ptr (trustMe (notNull ptr)) (trustMe (aligned ptr))
</code></pre>
<h1>Future directions</h1>
<p>Now, due to the way Idris 2 works, you don't actually <em>have</em> to spell out the proposition whenever you use <code>trustMe</code>. If you write <code>trustMe _</code>, then Idris will infer the appropriate type from context.</p>
<p>However, if you make a new language, then you can properly enforce this requirement of &quot;spelling everything out&quot; when you use the equivalent of <code>trustMe</code>.</p>
<p>Note that we can also actually write out proofs if we want to! It is also possible for some proofs to be inferred by the compiler (speaking more broadly). This can be more lightweight than you might expect. You can also push the proof obligations to the outermost level, and just pass around the proofs as you go deeper into the program (regardless of whether the proofs are ultimately originate as &quot;real&quot; or &quot;fake&quot;). These things are, in my opinion, a significant advantage over the approach where we never allow &quot;real&quot; proofs to be used. You could have a flag that causes the compiler to print out which obligations have real proofs and which are just assumed.</p>
<p>In my opinion, that last part is a very important point. If you disregard it entirely, then I believe you are missing out on a lot of extra power which could potentially be had at very low cost. If you do not want to use dependent types, you can separate the preconditions from function arguments.</p>
<h1>Credits</h1>
<p>Parts of this answer are inspired by a discussion I had with @EldritchConundrum in the chat <a href="https://chat.stackexchange.com/transcript/message/64809601#64809601">here</a>.</p>

CC BY-SA 4.0
2023-12-05T19:41:56.970Z
2023-12-05T19:55:24.123Z
2023-12-05T19:55:24.123Z
David Young
CC BY-SA 4.0
2023-12-05T19:57:55.787Z
You seem to be the first person who actually understood my question, thanks
mousetail 'he-him'
# Are there languages that implement a more granular precondition system than just safe/unsafe
Posted by: username_0 on 2023-12-02
In a language like C, many functions and operators have some preconditions to work. Violating a precondition is undefined behavior. For example, when indexing an array the index must be less than the length of the array. The compiler doesn't check this, it is up to the programmer.
In Rust, most functions always have defined behavior. Some functions are unsafe and require specific preconditions. Violating these preconditions results in undefined behavior. For example the Box::from_raw method states "For this to be safe, the memory must have been allocated in accordance with the memory layout used by Box."
However, this is still not an ideal situation. Each unsafe method has it's own unique set of required conditions to work properly. People often use unsafe just assuming what a function will do, but without carefully reading the documentation you can easily introduce undefined behavior.
Another issue is, suppose a unsafe function adds a precondition, there is no way to indicate this and check for it. For example, consider a hypothetical function that operates on pointers. It used to have some special case for null pointers but this is later deprecated and removed. Since the method is already unsafe existing code will still compile normally, just potentially fail in unexpected ways when used.
My question
I'm wondering if there is any more comprehensive safety system, that allows explicitly specifying pre-conditions in some structural way, then force users of the function to somehow acknowledge that they are aware of the requirements to run the code safely, in such a way that the code will break if a pre-condition is added which is not acknowledged.
An example of something I was thinking:
function dereference(pointer p)
    requires that p is not null
    requires that p is aligned
{
    ...
}

pointer p = get_pointer_from_somewhere()
I promise p is aligned
I promise p is not null
dereference(p)

Or something like this:
function mutate_object(object o)
  requires the object is not mutated in a different thread for the duration of this function {
    ...
}

I'm looking for prior art on the matter. Any languages that have something like this?
**Tags:** undefined-behavior
> **Comments:**
> **username_1**: My experience with Ada/SPARK preconditions was that I couldn't figure a way not to check them in productive code. Can't tell if that's what you are after here. For me, this was completely useless as most preconditions on "unsafe" code require expensive checks and some scaffolding that one would like to throw away in productive uses.  
> **username_1**: Another direction would be JML+Java. There, again, you'll eventually run into the issue that you need phantom memory to keep track of the status behind stuff that you are observing even if you do a formal proof. Also, proof systems make strange assumptions like memory never getting reused because it would break their assumptions on typing.  
> **username_2**: Take a look at Common Lisp's [Error Terminology](https://www.lispworks.com/documentation/lw61/CLHS/Body/01_db.htm) section.  
> **username_3**: Do refinement types count?  
> **username_0**: @Seggan No, those can be automatically checked by the compiler.  
> **username_4**: @mousetail Do you only want things that are not checked by the compiler? Also, when you say "can" be checked by the compiler, that probably includes quite a few things. "Cannot be checked by the compiler" (rather than "*is not* checked by the compiler) seems like a complex, and somewhat situation-dependent, requirement to me. Is that what you're looking for, though?  
> **username_5**: @mousetail I find your example somewhat specious, because being aligned and being non-null are things that can be modelled without much difficulty by a  traditional type system; can you expand on it?  That said, you may be interested in [design by contract](https://en.wikipedia.org/wiki/Design_by_contract) and [capabilities](https://en.wikipedia.org/wiki/Object-capability_model).  
---
## 4 answers
### Answer by username_4 on 2023-12-05. Score: 5 | Accepted answer
There are languages that support something very close to this. Consider Idris 2, for example.
How to write preconditions
You can represent preconditions as arguments. So, for example, if you have a function that takes a natural number and returns a natural number, but it requires its argument to be non-zero you could give it the type signature:
fn :
  (n : Nat) ->
  Not (n = 0) ->
  Nat
fn n proofNIsNonZero = ...

Since this "precondition" is just a regular argument, you can also pass this to other functions that require a non-negative natural number.
Easily conjuring fake proofs
Now, returning to the question. Idris 2 provides a feature that will unsafely convert a value of any type into a value of any other type. This "function" is called believe_me. We can use this to make a function called trustMe. This function will take a type and (unsafely) give back a value of that type. This can be used to conjure fake "proofs" of any proposition we want.
For more detail on how believe_me works in Idris, see this part of the documentation. I believe this is for Idris 1, but I don't think this has changed much between versions.
Here is an example of how you might do this. Note that, to use trustMe, you must generally spell out the proposition that you're "conjuring." I think this is what you're asking for in your question.
trustMe : (a : Type) -> a
trustMe _ = believe_me ()  -- We just use believe_me to convert the value of the Unit type into whatever type we need

data MyPtr : Type -> Type where
  MkMyPtr : Nat -> MyPtr a

notNull : MyPtr a -> Type
notNull (MkMyPtr x) = Not (x = 0)

-- This is just used in an example definition for @aligned@
-- so it's not necessary to understand this
data Even : Nat -> Type where
  EvenZ : Even 0                   -- 0 is even
  EvenS : Even x -> Even (S (S x)) -- If x is even, then x + 2 is even

-- Example definition: checks if the number is even
aligned : MyPtr a -> Type
aligned (MkMyPtr x) = Even x

dereference :
  (ptr : MyPtr a) ->
  notNull ptr ->
  aligned ptr ->
  a
dereference ptr notNullProof alignedProof = ?hole1

example : MyPtr a -> a
example ptr =
  dereference ptr (trustMe (notNull ptr)) (trustMe (aligned ptr))

Future directions
Now, due to the way Idris 2 works, you don't actually have to spell out the proposition whenever you use trustMe. If you write trustMe _, then Idris will infer the appropriate type from context.
However, if you make a new language, then you can properly enforce this requirement of "spelling everything out" when you use the equivalent of trustMe.
Note that we can also actually write out proofs if we want to! It is also possible for some proofs to be inferred by the compiler (speaking more broadly). This can be more lightweight than you might expect. You can also push the proof obligations to the outermost level, and just pass around the proofs as you go deeper into the program (regardless of whether the proofs are ultimately originate as "real" or "fake"). These things are, in my opinion, a significant advantage over the approach where we never allow "real" proofs to be used. You could have a flag that causes the compiler to print out which obligations have real proofs and which are just assumed.
In my opinion, that last part is a very important point. If you disregard it entirely, then I believe you are missing out on a lot of extra power which could potentially be had at very low cost. If you do not want to use dependent types, you can separate the preconditions from function arguments.
Credits
Parts of this answer are inspired by a discussion I had with @EldritchConundrum in the chat here.
> **Comments:**
> **username_0** (2023-12-05): You seem to be the first person who actually understood my question, thanks  
---
### Answer by username_6 on 2023-12-02. Score: 7
Eiffel
Eiffel is an object-oriented language in which functions and methods may have preconditions, specified using the require keyword:
my_list.do_all (agent (s: STRING)
     require
         not_void: s /= Void
     do
         s.append_character (',')
     ensure
         appended: s.count = old s.count + 1
     end)

As far as I know, Eiffel doesn't expose low-level details such as pointer alignment. However, it supports design by contract for higher-level preconditions such as that a reference is non-null ("not void" in Eiffel's terminology) or that a list is non-empty.
More details about Eiffel's design-by-contract features are given in the paper Avoid a Void: The eradication of null dereferencing by Meyer, Kogtenov & Stapf. In particular, the precondition can either be statically checked, or it can be asserted (with an exception thrown at runtime if the assertion fails). Assertions must be explicit at the call-site. However, assertions can be disabled at runtime, in which case they are the more granular "unsafe" labels you suggested
Java Modelling Language (JML)
JML is a language used to specify properties of Java programs, such that the specifications can be checked by tools such as OpenJML or KeY. Preconditions can be written in comments; for example, here's binary search:
//@ requires sortedArray != null && 0 < sortedArray.length < Integer.MAX_VALUE;
//@ requires \forall int i; 0 <= i < sortedArray.length; \forall int j; i < j < sortedArray.length; sortedArray[i] <= sortedArray[j];
//@ old boolean containsValue = (\exists int i; 0 <= i < sortedArray.length; sortedArray[i] == value);
//@ ensures containsValue <==> 0 <= \result < sortedArray.length;
//@ ensures !containsValue <==> \result == -1;
//@ pure
public static int search(int[] sortedArray, int value) {
    // ...
}

The first two lines, annotated //@ requires, are the preconditions: in this example, that the array is non-null and non-empty, and that the array elements are in ascending order.
Like Eiffel, these preconditions will be checked for each call-site, and preconditions which can't be proven statically can still be asserted using assert statements. Like Eiffel, Java has the option to disable assertions at runtime.
---
### Answer by username_7 on 2023-12-04. Score: 2
Your example is already pretty much C++
void dereference(T& p)
    // requires that p is not null
    // requires that p is aligned
{
    std::cout << p;
}

void* pv = get_pointer_from_somewhere()
T* pt = reinterpret_cast(pv); // I promise p is aligned, and points to a T
T& rt = *pt; // I promise p is not null
dereference(rt);

As usual, breaking a promise leads to Undefined Behavior.
This is an example where C++ just happens to encode the example preconditions in the existing type system. But C++ has a Turing-complete concept system that allows library writes to introduce new named concepts. See for instance this StackOverflow question which introduces a CanMakeSharedFromThis concept to check if a type supports a kind of smart pointers.
---
### Answer by username_8 on 2023-12-04. Score: -1
Any language with monads and pattern matching (Haskell) can achieve this. A function with type `Maybe a` can explicitly pattern pre-condition failures and returning `Nothing` instead of `Just a`. Because code using the resulting Maybe has to extract the resulting Nothing or a it's required to acknowledge the Nothing post-condition.

Likewise Rust has `Option`, but I'm not familiar enough with Rust to know if Option is escapable.
> **Comments:**
> **username_0** (2023-12-04): In these cases it is impossible to tell if the condition has been met, it's undefined behavior. Returning `None` would make the behavior defined. Which is better of course but not always possible  
> **username_4** (2023-12-04): @mousetail Hmm, maybe I misunderstand something but aren't both of the examples in the question checkable (at runtime)? Alignment is a bit trickier since it's architecture dependent, but if you can figure out what the architecture wants addresses aligned to then you can just do a divisibility check. The non-null condition is definitely checkable.  
> **username_0** (2023-12-04): @DavidYoung It's more about not wanting to check at runtime (due to performance cost or it just being unnecessary) than being unable to. However, I want to use this also for conditions that are actually impossible to check at runtime.  
> **username_6** (2023-12-04): @mousetail I think the point is really that preconditions can be expressed in the language's type system, rather than having a separate system for them. For cases where the precondition is not feasible to prove and you don't want a check at runtime, then Rust's `unwrap_unchecked()` (e.g. on an Option) gives the desired result: no runtime cost, and the code 'documenting' the assertion appears in the relevant place.  
> **username_4** (2023-12-04): @mousetail You can do a lot with type system features. For example, Haskell has a feature called `newtype`. It's a zero-cost wrapper around a type (the wrapper only exists at compile time). The type checker considers it distinct from the original type. One simple usage is to define a `NotNull` type, which can never be set to null (say, created by `malloc`, you can only add non-negative integers to it, you can assign a `NotNull` to a `NotNull`, etc). You can do more complex things too, like ensuring a list is sorted before being merged. See [this](https://kataskeue.com/gdp.pdf)  
> **username_4** (2023-12-04): And if you really want to crash rather than having a check, it's best to crash early. So, instead of having something like a function `fn` that takes a pointer that must be non-null and crashes (or UB) otherwise, have `fn` take a `NotNull` and provide an unsafe way to make a `NotNull` (ideally that crashes right away if it's null), ideally only used at the highest level. This can be zero-cost. Even better, if you can stand the slight performance reduction, don't make it crash or give UB at all and just handle the null pointer case at the highest level in the code and provide a safe interface.  
> **username_8** (2023-12-05): @mousetail by it's nature you can not detect undefined behavior.  What happens is *undefined*.  Including overriding any possible check, or acting in completely unpredictable ways.

What you want, "not wanting to check at runtime" is not possible.  There is no free lunch to be had here.  If the code has dynamic values at runtime then it requires dynamic checks of those values to see if they're within precondition bounds.  
> **username_0** (2023-12-05): @DanielN I don't want to detect undefined behavior. I just want some explicit way for programmers to be able to explain how they have met the conditions to avoid undefined behavior, when the compiler can't check it. And make sure the code breaks when the conditions change  
---
