<p>Some languages support design by contract in the language itself.</p>
<p>The absolute bare minimum for this is to define:</p>
<ul>
<li>pre-conditions   (expects)</li>
<li>post-conditions  (ensures) &amp;</li>
<li>invariants</li>
</ul>
<p>These are often added as library primitives rather than as part of the language.
Adding them to the language gives us the potential for:</p>
<ul>
<li>checking them at compile time</li>
<li>running a separate verifier program to formal prove some parts of our specification.</li>
</ul>
<p>A language I am aware of that trys to support this is <a href="https://dafny.org/" rel="noreferrer">Dafny</a>,
which describes itself as a <code>verification-aware programming language</code></p>
<p>On the functional side there are things such as <a href="https://www.mn.uio.no/ifi/english/research/groups/psy/completedmasters/2019/kolstad/" rel="noreferrer">liquid haskell</a> and
<a href="https://docs.idris-lang.org/en/latest/tutorial/theorems.html" rel="noreferrer">Idris</a></p>
<p>Then there are also fully fledged proof assistants like <a href="https://coq.inria.fr/" rel="noreferrer">coq</a> which I'm not sure count as &quot;general purpose&quot; languages due to their high level of specialisation.</p>
<p>C++ has also gone a little way in this direction.
The standard recently added:</p>
<ul>
<li><a href="https://en.wikipedia.org/wiki/Concepts_(C%2B%2B)" rel="noreferrer">concepts aka concepts-lite</a></li>
</ul>
<p>Plans to add</p>
<ul>
<li><a href="https://www.modernescpp.com/index.php/c-core-guidelines-a-detour-to-contracts" rel="noreferrer">contracts</a></li>
</ul>
<p>are in the works.
And</p>
<ul>
<li>'full' concepts including <code>concept maps</code> and <code>axioms</code></li>
</ul>
<p>were put on hold.</p>
<p>Concepts and contracts elevate design by contract from something typically added via library functions to part of the language that would in theory allow the compiler to use a solver like <a href="https://github.com/Z3Prover/z3/wiki" rel="noreferrer">Z3</a>.</p>
<p>Example contracts syntax:</p>
<pre class="lang-c prettyprint-override"><code>int mul(int x, int y)
  [[expects: x &gt; 0]]         // implicit default
  [[expects default: y &gt; 0]]
  [[ensures audit res: res &gt; 0]]{
  return x * y;
}
</code></pre>
<p>For concepts see for example <a href="https://en.cppreference.com/w/cpp/language/constraints" rel="noreferrer">https://en.cppreference.com/w/cpp/language/constraints</a></p>
<p><strong>What strategies are there for supporting <a href="https://en.wikipedia.org/wiki/Formal_verification" rel="noreferrer">formal verification</a> in a programming language and
what are their pros and cons?</strong></p>
<p>I asked a related question here: <a href="https://proofassistants.stackexchange.com/q/2225/2432">What is needed to move from design by contract to using a more advanced prover?</a></p>

<verification>
What options are there for adding formal verification to a general purpose programming language?
CC BY-SA 4.0
2023-06-08T15:45:25.477Z
Kotlin has a contracts feature too (although it is in the experimental phase). This allows for stuff like "if I'm passed a null, I return a null", and for the type checker to take note of that
Seggan
CC BY-SA 4.0
2023-06-09T11:30:42.100Z
I couldn't see the justification for removing the link to the related question so I've re-added it. If you want it removed please explain why.
Bruce Adams
<h2><a href="https://en.wikipedia.org/wiki/Hoare_logic" rel="nofollow noreferrer">Hoare Logic</a></h2>
<p>AKA Axiomatic Semantics, or what you call <a href="https://en.wikipedia.org/wiki/Design_by_contract" rel="nofollow noreferrer">&quot;Design-by-Contract&quot;</a>. It was later refined into the Weakest Precondition Calculus by E. W. Dijkstra.</p>
<p>Relatively recently John Reynolds developed it yet further into <a href="https://en.wikipedia.org/wiki/Separation_logic" rel="nofollow noreferrer">Separation Logic</a> opening the door for reasoning about <em>mutable references</em> (or pointers), and then Peter O'Hearn evolved it into Concurrent Separation Logic.</p>
<p>These logics or variations thereof form the basis of vast majority of verification tools and frameworks. Most notably, <a href="https://frama-c.com" rel="nofollow noreferrer">Frama-C</a>, <a href="https://compcert.org" rel="nofollow noreferrer">CompCert</a>, <a href="https://why3.lri.fr" rel="nofollow noreferrer">Why3</a>, aforementioned Dafny and so on.</p>
<h2><a href="https://en.wikipedia.org/wiki/Model_checking" rel="nofollow noreferrer">(Bounded) Model-Checking</a></h2>
<p>A Model Checker either finds a model with required properties or proves no such model could ever exist. When the model is a (possible) trace of a program execution, a Model Checker can prove that the program never reaches a bad state or provide a counterexample: exact sequence of steps leading to the bad state.</p>
<p>The most basic definition of a &quot;bad state&quot; is a program crash. It might be refined into an unhandled exception, out-of-bounds access, null pointed dereference and so on. The upside is you don't need to specify anything more beyond the language's semantics to check this property.</p>
<p>With minimal additional cleverness we can check that program never executes <code>assert(false)</code>, and this lets us verify more interesting invariants than simply &quot;the program doesn't crash&quot; while staying within the vanilla language as long as most languages have <code>assert</code> statements built-in. With Symbolic Model Checking we can verify more complex asserts than simply <code>assert(false)</code> and in a more precise way.</p>
<p>The major obstacle to complete model checking is loops, because it's hard to tell the number of iterations in advance. Hence the use of <strong>Bounded</strong> Model Checking, which essentially unrolls the loops a finite number of steps.</p>
<p>Overall Model Checking provides huge benefits almost &quot;for free&quot;, thus wide variety of Model Checking based tools for many languages with different scopes and capabilities.</p>
<h2><a href="https://en.wikipedia.org/wiki/Abstract_interpretation" rel="nofollow noreferrer">Abstract Interpretation</a></h2>
<p>Abstract Interpretation presents a very general framework not only for verification, but almost any program transformations: one can formulate <em>compilation</em> as a sort of Abstract Interpretation if squints hard enough! </p>
<p>Thus again there are a sizeable variety of Abstract Interpretation based tools checking all kinds of program properties, from Python and JavaScript types to Web applications vulnerabilities. But to check more advanced properties one first have to <em>specify</em> these properties. And for specification we often reuse Hoare-style logic or something similar.</p>

CC BY-SA 4.0
2023-06-19T09:08:47.890Z
2023-06-19T09:08:47.890Z
Alex Chichigin
<h1>Refinement Types</h1>
<p>A refinement type is a type with a predicate attached, and all instances must satisfy the predicate.</p>
<p>In Liquid Haskell they're denoted as <code>{ x:T | f(x) }</code>, where the type <code>T</code> is refined by the predicate <code>f</code>. In Flux they're denoted <code>T{x:f(x)}</code>, e.g. <code>i32{v:n &lt;= v}</code>. Though both languages have additional syntax to support more invariants</p>
<h2>Examples</h2>
<h3>Liquid Haskell</h3>
<ul>
<li><p><code>{ n:Int | 0 &lt;= n &amp;&amp; n &lt; 10 }</code>: an integer in the range <code>[0, 10)</code></p>
</li>
<li><p><code>{ xs:[String] | isSorted xs }</code>: a list of strings which is guaranteed sorted</p>
</li>
<li><p><code>merge :: (Ord a) =&gt; x:[a] -&gt; y:[a] -&gt; { v:[a] | (UnionElts v x y) }</code>: a function which takes 2 lists and returns a list containing all elements from both</p>
</li>
</ul>
<h3>Flux</h3>
<pre class="lang-rust prettyprint-override"><code>#[flux::sig(fn (n:i32) -&gt; i32{v:0&lt;=v &amp;&amp; n&lt;=v})]
pub fn abs(n: i32) -&gt; i32 {
    if 0 &lt;= n {
        n
    } else {
        0 - n
    }
}
</code></pre>
<p>Takes an integer <code>n</code> and returns an integer which is both non-negative (<code>0&lt;=v</code>) and greater-than-or-equal-to <code>n</code> (<code>n&lt;=v</code>).</p>
<pre class="lang-rust prettyprint-override"><code>#[flux::trusted]
#[flux::sig(fn(self: &amp;strg RVec&lt;T&gt;[@n], T)
            ensures self: RVec&lt;T&gt;[n+1])]
pub fn push(&amp;mut self, item: T) {
    self.inner.push(item);
}
</code></pre>
<p>Takes a vector initially of size <code>n</code> and an element, and after returning, the vector is of size <code>n + 1</code>.</p>
<h2>Implementations</h2>
<ul>
<li><p><a href="https://flux-rs.github.io/flux/" rel="noreferrer">Flux</a> (Rust)</p>
</li>
<li><p><a href="https://ucsd-progsys.github.io/liquidhaskell/" rel="noreferrer">Liquid Haskell</a></p>
</li>
<li><p><a href="https://blog.racket-lang.org/2017/11/adding-refinement-types.html" rel="noreferrer">Refinement Types in Typed Racket</a></p>
</li>
<li><p><a href="https://github.com/fthomas/refined" rel="noreferrer">Refined</a> (Scala)</p>
</li>
<li><p><a href="https://catarinagamboa.github.io/liquidjava.html" rel="noreferrer">Liquid Java</a></p>
</li>
<li><p><a href="https://www.microsoft.com/en-us/research/project/f7-refinement-types-for-f/" rel="noreferrer">F7</a> (F#)</p>
</li>
<li><p><a href="https://github.com/UCSD-PL/refscript" rel="noreferrer">refscript</a> and <a href="https://github.com/jedahu/ts-refined" rel="noreferrer">ts-refind</a> (TypeScript)</p>
</li>
<li><p><a href="https://blag.cedeela.fr/simple-refinement-types-for-ocaml/" rel="noreferrer">Simple refinement types for ocaml</a></p>
</li>
</ul>
<h2>Pros</h2>
<ul>
<li><p>Intuitive, at least at the surface-level. Many proofs require constructing proofs-as-data which can be very confusing. Refinement types are simply types with predicates, and the predicates are simply expressions in the base language. It's much easier to write <code>{ xs:[String] | isSorted xs }</code> than it is to define an inductive ADT which can only represent sorted lists. However, proving that these predicates hold is less intuitive...</p>
</li>
<li><p>Pure superset of the language, you simply add extra annotations. The code can still be processed by the base compiler/interpreter if the annotations are comments (which they usually are)</p>
</li>
<li><p>Doesn't require much changes to the type system, you simply add an optional predicate to every type. The refinement type system is not very complicated, at least at the surface-level and before adding extensions to prove stronger properties</p>
</li>
</ul>
<h2>Cons</h2>
<ul>
<li><p>Not very strong, generally suited for simple proofs like bounded numbers (e.g. for array indexing)</p>
</li>
<li><p>Many implementations add extensions on top of the refinement types to prove stronger properties (see first point)</p>
</li>
<li><p>Sometimes the compiler can't type-check the refinements, and you must rewrite the predicates in unintuitive and/or verbose ways, and/or provide unintuitive and/or verbose lemmas. It can be difficult and seem archaic even for programmers familiar with theorem proving, if they're familiar with languages like Coq where the proofs are more straightforward (albeit also verbose)</p>
</li>
<li><p>Verbose. You're adding extra annotations to a program, and often you must add a lot of these annotations in order to have enough info to prove useful properties. Not to mention writing extra helper functions and lemmas, and &quot;simplifying&quot; your existing functions (actually making them more verbose), to satisfy the solver. Although unfortunately verbosity is a con in most formal methods...</p>
</li>
</ul>
<h2>Consensus</h2>
<p>So far it sees that the general consensus is that refinement types are great for proving array bounds, sortedness, and other simple properties. However, they can't prove more advanced properties on their own. Personally, I couldn't find any example of a large project which used refinement types; the largest I could find is in the paper <a href="https://goto.ucsd.edu/%7Envazou/real_world_liquid.pdf" rel="noreferrer"><em>LiquidHaskell: Experience with
Refinement Types in the Real World</em></a>, where the Liquid Haskell developers add liquid types to over 10,000 lines of code in popular libraries on Hackage.</p>
<p>The most popular implementation of refinement types is <a href="https://ucsd-progsys.github.io/liquidhaskell/" rel="noreferrer">Liquid Haskell</a>. <a href="https://flux-rs.github.io/flux/" rel="noreferrer">Flux</a> is an upcoming system which will be presented at <a href="https://pldi23.sigplan.org/" rel="noreferrer">PLDI 2023</a>, so you may want to keep an eye on that.</p>
<ul>
<li>types projects</li>
</ul>
<h2>See also</h2>
<ul>
<li><a href="https://arxiv.org/pdf/2010.07763.pdf" rel="noreferrer">Refinement Types: A Tutorial</a></li>
</ul>

CC BY-SA 4.0
2023-06-08T03:15:46.087Z
2023-06-08T03:40:44.227Z
2023-06-08T03:40:44.227Z
tarzh
CC BY-SA 4.0
2023-06-08T07:55:47.043Z
It seems to me that concepts in C++ (which are really just sugar over templates) count as refinement types. Would you agree?
Bruce Adams
CC BY-SA 4.0
2023-06-08T07:58:15.333Z
Could you give some examples of features required/missing for the stronger proofs you mention? I think that overlaps somewhat with my question [here](https://proofassistants.stackexchange.com/questions/2225/what-is-needed-to-move-from-design-by-contract-to-using-a-proof-assistant) . My guess would be maybe quantification operators like `forall` and `exists`.
Bruce Adams
CC BY-SA 4.0
2023-06-08T19:01:18.947Z
Reading around my related question https://proofassistants.stackexchange.com/questions/2225/what-is-needed-to-move-from-design-by-contract-to-using-a-proof-assistant - suggests that refinement types alone are insufficient. You might also need, at least optionally, [soundness](https://en.wikipedia.org/wiki/Soundness) and [totality](https://docs.idris-lang.org/en/latest/tutorial/theorems.html#sect-totality)
Bruce Adams
CC BY-SA 4.0
2023-06-11T09:35:59.787Z
"The refinement type system is not very complicated" — yeah, no more than Dependent Types... :) Originally Refinement Types in F* were formalized without full-blown Dependent Types, but with 4 sorts of kinds, which not very simple by my standards. Still later they "gave up" and went with "honest" Dependent Types (though using extensional theory).
Alex Chichigin
CC BY-SA 4.0
2023-06-11T09:42:10.913Z
"I couldn't find any example of a large project which used refinement types" — https://project-everest.github.io is the most well-known and widely-deployed (Windows, Azure, Chrome) I guess...
Alex Chichigin
# What options are there for adding formal verification to a general purpose programming language?
Posted by: username_0 on 2023-06-08
Some languages support design by contract in the language itself.
The absolute bare minimum for this is to define:

pre-conditions   (expects)
post-conditions  (ensures) &
invariants

These are often added as library primitives rather than as part of the language.
Adding them to the language gives us the potential for:

checking them at compile time
running a separate verifier program to formal prove some parts of our specification.

A language I am aware of that trys to support this is Dafny,
which describes itself as a verification-aware programming language
On the functional side there are things such as liquid haskell and
Idris
Then there are also fully fledged proof assistants like coq which I'm not sure count as "general purpose" languages due to their high level of specialisation.
C++ has also gone a little way in this direction.
The standard recently added:

concepts aka concepts-lite

Plans to add

contracts

are in the works.
And

'full' concepts including concept maps and axioms

were put on hold.
Concepts and contracts elevate design by contract from something typically added via library functions to part of the language that would in theory allow the compiler to use a solver like Z3.
Example contracts syntax:
int mul(int x, int y)
  [[expects: x > 0]]         // implicit default
  [[expects default: y > 0]]
  [[ensures audit res: res > 0]]{
  return x * y;
}

For concepts see for example https://en.cppreference.com/w/cpp/language/constraints
What strategies are there for supporting formal verification in a programming language and
what are their pros and cons?
I asked a related question here: What is needed to move from design by contract to using a more advanced prover?
**Tags:** verification
> **Comments:**
> **username_1**: Kotlin has a contracts feature too (although it is in the experimental phase). This allows for stuff like "if I'm passed a null, I return a null", and for the type checker to take note of that  
> **username_0**: I couldn't see the justification for removing the link to the related question so I've re-added it. If you want it removed please explain why.  
---
## 2 answers
### Answer by username_3 on 2023-06-08. Score: 14
Refinement Types
A refinement type is a type with a predicate attached, and all instances must satisfy the predicate.
In Liquid Haskell they're denoted as { x:T | f(x) }, where the type T is refined by the predicate f. In Flux they're denoted T{x:f(x)}, e.g. i32{v:n <= v}. Though both languages have additional syntax to support more invariants
Examples
Liquid Haskell

{ n:Int | 0 <= n && n < 10 }: an integer in the range [0, 10)

{ xs:[String] | isSorted xs }: a list of strings which is guaranteed sorted

merge :: (Ord a) => x:[a] -> y:[a] -> { v:[a] | (UnionElts v x y) }: a function which takes 2 lists and returns a list containing all elements from both


Flux
#[flux::sig(fn (n:i32) -> i32{v:0<=v && n<=v})]
pub fn abs(n: i32) -> i32 {
    if 0 <= n {
        n
    } else {
        0 - n
    }
}

Takes an integer n and returns an integer which is both non-negative (0<=v) and greater-than-or-equal-to n (n<=v).
#[flux::trusted]
#[flux::sig(fn(self: &strg RVec[@n], T)
            ensures self: RVec[n+1])]
pub fn push(&mut self, item: T) {
    self.inner.push(item);
}

Takes a vector initially of size n and an element, and after returning, the vector is of size n + 1.
Implementations

Flux (Rust)

Liquid Haskell

Refinement Types in Typed Racket

Refined (Scala)

Liquid Java

F7 (F#)

refscript and ts-refind (TypeScript)

Simple refinement types for ocaml


Pros

Intuitive, at least at the surface-level. Many proofs require constructing proofs-as-data which can be very confusing. Refinement types are simply types with predicates, and the predicates are simply expressions in the base language. It's much easier to write { xs:[String] | isSorted xs } than it is to define an inductive ADT which can only represent sorted lists. However, proving that these predicates hold is less intuitive...

Pure superset of the language, you simply add extra annotations. The code can still be processed by the base compiler/interpreter if the annotations are comments (which they usually are)

Doesn't require much changes to the type system, you simply add an optional predicate to every type. The refinement type system is not very complicated, at least at the surface-level and before adding extensions to prove stronger properties


Cons

Not very strong, generally suited for simple proofs like bounded numbers (e.g. for array indexing)

Many implementations add extensions on top of the refinement types to prove stronger properties (see first point)

Sometimes the compiler can't type-check the refinements, and you must rewrite the predicates in unintuitive and/or verbose ways, and/or provide unintuitive and/or verbose lemmas. It can be difficult and seem archaic even for programmers familiar with theorem proving, if they're familiar with languages like Coq where the proofs are more straightforward (albeit also verbose)

Verbose. You're adding extra annotations to a program, and often you must add a lot of these annotations in order to have enough info to prove useful properties. Not to mention writing extra helper functions and lemmas, and "simplifying" your existing functions (actually making them more verbose), to satisfy the solver. Although unfortunately verbosity is a con in most formal methods...


Consensus
So far it sees that the general consensus is that refinement types are great for proving array bounds, sortedness, and other simple properties. However, they can't prove more advanced properties on their own. Personally, I couldn't find any example of a large project which used refinement types; the largest I could find is in the paper LiquidHaskell: Experience with
Refinement Types in the Real World, where the Liquid Haskell developers add liquid types to over 10,000 lines of code in popular libraries on Hackage.
The most popular implementation of refinement types is Liquid Haskell. Flux is an upcoming system which will be presented at PLDI 2023, so you may want to keep an eye on that.

types projects

See also

Refinement Types: A Tutorial
> **Comments:**
> **username_0** (2023-06-08): It seems to me that concepts in C++ (which are really just sugar over templates) count as refinement types. Would you agree?  
> **username_0** (2023-06-08): Could you give some examples of features required/missing for the stronger proofs you mention? I think that overlaps somewhat with my question [here](https://proofassistants.stackexchange.com/questions/2225/what-is-needed-to-move-from-design-by-contract-to-using-a-proof-assistant) . My guess would be maybe quantification operators like `forall` and `exists`.  
> **username_0** (2023-06-08): Reading around my related question https://proofassistants.stackexchange.com/questions/2225/what-is-needed-to-move-from-design-by-contract-to-using-a-proof-assistant - suggests that refinement types alone are insufficient. You might also need, at least optionally, [soundness](https://en.wikipedia.org/wiki/Soundness) and [totality](https://docs.idris-lang.org/en/latest/tutorial/theorems.html#sect-totality)  
> **username_2** (2023-06-11): "The refinement type system is not very complicated" — yeah, no more than Dependent Types... :) Originally Refinement Types in F* were formalized without full-blown Dependent Types, but with 4 sorts of kinds, which not very simple by my standards. Still later they "gave up" and went with "honest" Dependent Types (though using extensional theory).  
> **username_2** (2023-06-11): "I couldn't find any example of a large project which used refinement types" — https://project-everest.github.io is the most well-known and widely-deployed (Windows, Azure, Chrome) I guess...  
---
### Answer by username_2 on 2023-06-19. Score: 3
## [Hoare Logic](https://en.wikipedia.org/wiki/Hoare_logic)

AKA Axiomatic Semantics, or what you call ["Design-by-Contract"](https://en.wikipedia.org/wiki/Design_by_contract). It was later refined into the Weakest Precondition Calculus by E. W. Dijkstra.

Relatively recently John Reynolds developed it yet further into [Separation Logic](https://en.wikipedia.org/wiki/Separation_logic) opening the door for reasoning about *mutable references* (or pointers), and then Peter O'Hearn evolved it into Concurrent Separation Logic.

These logics or variations thereof form the basis of vast majority of verification tools and frameworks. Most notably, [Frama-C](https://frama-c.com), [CompCert](https://compcert.org), [Why3](https://why3.lri.fr), aforementioned Dafny and so on.

## [(Bounded) Model-Checking](https://en.wikipedia.org/wiki/Model_checking)

A Model Checker either finds a model with required properties or proves no such model could ever exist. When the model is a (possible) trace of a program execution, a Model Checker can prove that the program never reaches a bad state or provide a counterexample: exact sequence of steps leading to the bad state.

The most basic definition of a "bad state" is a program crash. It might be refined into an unhandled exception, out-of-bounds access, null pointed dereference and so on. The upside is you don't need to specify anything more beyond the language's semantics to check this property.

With minimal additional cleverness we can check that program never executes `assert(false)`, and this lets us verify more interesting invariants than simply "the program doesn't crash" while staying within the vanilla language as long as most languages have `assert` statements built-in. With Symbolic Model Checking we can verify more complex asserts than simply `assert(false)` and in a more precise way.

The major obstacle to complete model checking is loops, because it's hard to tell the number of iterations in advance. Hence the use of **Bounded** Model Checking, which essentially unrolls the loops a finite number of steps.

Overall Model Checking provides huge benefits almost "for free", thus wide variety of Model Checking based tools for many languages with different scopes and capabilities.

## [Abstract Interpretation](https://en.wikipedia.org/wiki/Abstract_interpretation)

Abstract Interpretation presents a very general framework not only for verification, but almost any program transformations: one can formulate *compilation* as a sort of Abstract Interpretation if squints hard enough!

Thus again there are a sizeable variety of Abstract Interpretation based tools checking all kinds of program properties, from Python and JavaScript types to Web applications vulnerabilities. But to check more advanced properties one first have to *specify* these properties. And for specification we often reuse Hoare-style logic or something similar.
---
