<p>Hi Theoretical Computer Science Stack Exchange,</p>
<p>I have been wondering if there are programming languages where one can have constraints on values variables can have?
Have such approach been used in programming language research? I'm aware of testing, static analysis, model checking, and
formal verification and was thinking if constrains, like in optimization, would provide another approach for building
better quality software.</p>
<ol>
<li>(Example 1)
Suppose we want to define a data structure for circle, using doubles. Since unsigned double does not exist in C,
one could have (modified C syntax below)</li>
</ol>
<pre><code>struct circle {
    double x;;
    double y;;
    double radius; radius &gt;= 0;
}
</code></pre>
<p>As you can see, the constraints are placed between ';' symbols. The idea is to ensure correctness/validity of
the values of a circle when constraint checking is on.</p>
<ol start="2">
<li>(Example 2)
Suppose we want to implement an closed interval in <span class="math-container">$double$</span> with a point in it. Something like</li>
</ol>
<pre><code>struct closed_interval_and_point {
    double min;;
    double max;;
    double point; min &lt;= point &amp;&amp; point &lt;= max;
}
</code></pre>
<p>This example motivates unlock and lock features for constraint checking. To modify interval a point might lie outside the
interval for a moment. Something like</p>
<pre><code>struct closed_interval_and_point var = {.min = 0.0f, .max = 1.0f, .point = 0.5f};;
unlock var.point;; // unlock constraint checking for var.point
var.min = 2.0f;;
var.max = 4.0f;;
var.point = 3.0f;;
lock var.point;; // lock constraint checking for var.point
</code></pre>
<p>might be used to enable modification of structure. Constraint checking would be off after unlock and done after lock
command and after it. (One could also replace unlock by off and lock by on, perhaps those keywords would be better,
here I just describe the idea).</p>
<ol start="3">
<li><p>(Idea 1)
Constraint checking could be implemented using valgrind style environment, where each modification to memory address can be
tracked. Every time a value in memory changes, the language would check the constraints related to the value, in case
constraint checking is locked.</p>
</li>
<li><p>(Idea 2)
The idea of extending C with constraints is that once one has run program with multiple inputs with no constraint violations,
one could extract a normal C program which does not have constraint checks, but which has been &quot;validated&quot; in the constrained
environment.</p>
</li>
<li><p>(Question 1)
Has this approach been researched in academia or industry? If so, what is the keyword for finding this kind of languages/extensions?
If not, I think this approach could be fundamentally different(?) than testing, debugging, static analysis, model checking and formal verification.
Of course, I have no data to show that this constraint approach would be successful/useful.</p>
</li>
<li><p>(Question 2)
I know my examples are incomplete in detail. I believe that a complete discussion of the subject is inappropriate in this forum.
Where could I discuss this idea further?</p>
</li>
</ol>
<p>Best Regards,</p>
<p>Tomi Pannila</p>
<p>Errata : Valgrind -&gt; GDB watchpoint</p>

CC BY-SA 4.0
2022-04-21T18:40:21.780Z
Don't dependent types, refinement types, liquid types do what you have in mind? See e.g. [Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell-blog/).
Martin Berger
CC BY-SA 4.0
2022-04-22T08:05:56.380Z
Yes, I think a relevant keyword here is "refinement types".  There is a [very short Wikipedia entry](https://en.wikipedia.org/wiki/Refinement_type) about them, searching Google should give you more detailed results.
Damiano Mazza
CC BY-SA 4.0
2022-04-23T14:09:34.723Z
Hi @Martin_Berger and Damiano_Mazza,

Both "refinement type" and "dependent type" seem to be correct.
Than you for referring to Liquid Haskell, RefinedC seemed also interesting. I was looking for a mainstream imperative language embedded with easy to use constraints on values. I see there is active research on the subject "refinement types", and implementations related to it, so I hope that in future we will see refinement types motivated prototypes brought to at least C structs, C++ classes and Java classes for structural soundness checks, not full formal verification.
Tomi Pannila
CC BY-SA 4.0
2022-05-03T06:33:31.263Z
Since version 8.0, C# has non-nullable reference types. This is incredibly useful in my day job. Does this fit the bill? https://docs.microsoft.com/en-us/dotnet/csharp/nullable-references
Hermann Gruber
CC BY-SA 4.0
2022-06-07T11:01:01.453Z
@HermannGruber NRTs in C# 8.0+ are not an example of general-purpose or arbitrary constraints: all they can do is _hint_, but not yet _prove_, that a reference-type or `Nullable<T>` parameter, local, or field _is_, _is-not_, or _might-be_ `null` (or `default` in the case of `Nullable<T>`). Fortunately (in most, but not all cases) you can instead implement those class's object state invariant constraints in the class' constructor - but this still requires runtime checks: the compiler itself cannot evaluate (and flow, and _elide_, where possible) those constraints' runtime assertions.
Dai
CC BY-SA 4.0
2022-06-08T10:07:44.180Z
@Dai thanks for the clarification!
Hermann Gruber
<reference-request><pl.programming-languages>
Programming languages with constraints on values of variables?
Tomi Pannila
# Programming languages with constraints on values of variables?

(Asked by: username_0 on 2022-04-21)

Hi Theoretical Computer Science Stack Exchange,
I have been wondering if there are programming languages where one can have constraints on values variables can have?
Have such approach been used in programming language research? I'm aware of testing, static analysis, model checking, and
formal verification and was thinking if constrains, like in optimization, would provide another approach for building
better quality software.

(Example 1)
Suppose we want to define a data structure for circle, using doubles. Since unsigned double does not exist in C,
one could have (modified C syntax below)

struct circle {
    double x;;
    double y;;
    double radius; radius >= 0;
}

As you can see, the constraints are placed between ';' symbols. The idea is to ensure correctness/validity of
the values of a circle when constraint checking is on.

(Example 2)
Suppose we want to implement an closed interval in $double$ with a point in it. Something like

struct closed_interval_and_point {
    double min;;
    double max;;
    double point; min <= point && point <= max;
}

This example motivates unlock and lock features for constraint checking. To modify interval a point might lie outside the
interval for a moment. Something like
struct closed_interval_and_point var = {.min = 0.0f, .max = 1.0f, .point = 0.5f};;
unlock var.point;; // unlock constraint checking for var.point
var.min = 2.0f;;
var.max = 4.0f;;
var.point = 3.0f;;
lock var.point;; // lock constraint checking for var.point

might be used to enable modification of structure. Constraint checking would be off after unlock and done after lock
command and after it. (One could also replace unlock by off and lock by on, perhaps those keywords would be better,
here I just describe the idea).

(Idea 1)
Constraint checking could be implemented using valgrind style environment, where each modification to memory address can be
tracked. Every time a value in memory changes, the language would check the constraints related to the value, in case
constraint checking is locked.

(Idea 2)
The idea of extending C with constraints is that once one has run program with multiple inputs with no constraint violations,
one could extract a normal C program which does not have constraint checks, but which has been "validated" in the constrained
environment.

(Question 1)
Has this approach been researched in academia or industry? If so, what is the keyword for finding this kind of languages/extensions?
If not, I think this approach could be fundamentally different(?) than testing, debugging, static analysis, model checking and formal verification.
Of course, I have no data to show that this constraint approach would be successful/useful.

(Question 2)
I know my examples are incomplete in detail. I believe that a complete discussion of the subject is inappropriate in this forum.
Where could I discuss this idea further?


Best Regards,
Tomi Pannila
Errata : Valgrind -> GDB watchpoint

**Tags:** reference-request, pl.programming-languages
> **Comments:**
> **username_1**: Don't dependent types, refinement types, liquid types do what you have in mind? See e.g. [Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell-blog/).  
> **username_2**: Yes, I think a relevant keyword here is "refinement types".  There is a [very short Wikipedia entry](https://en.wikipedia.org/wiki/Refinement_type) about them, searching Google should give you more detailed results.  
> **username_0**: Hi @Martin_Berger and Damiano_Mazza,  Both "refinement type" and "dependent type" seem to be correct. Than you for referring to Liquid Haskell, RefinedC seemed also interesting. I was looking for a mainstream imperative language embedded with easy to use constraints on values. I see there is active research on the subject "refinement types", and implementations related to it, so I hope that in future we will see refinement types motivated prototypes brought to at least C structs, C++ classes and Java classes for structural soundness checks, not full formal verification.  
> **username_3**: Since version 8.0, C# has non-nullable reference types. This is incredibly useful in my day job. Does this fit the bill? https://docs.microsoft.com/en-us/dotnet/csharp/nullable-references  
> **username_4**: @HermannGruber NRTs in C# 8.0+ are not an example of general-purpose or arbitrary constraints: all they can do is _hint_, but not yet _prove_, that a reference-type or `Nullable<T>` parameter, local, or field _is_, _is-not_, or _might-be_ `null` (or `default` in the case of `Nullable<T>`). Fortunately (in most, but not all cases) you can instead implement those class's object state invariant constraints in the class' constructor - but this still requires runtime checks: the compiler itself cannot evaluate (and flow, and _elide_, where possible) those constraints' runtime assertions.  
> **username_3**: @Dai thanks for the clarification!  

---

## 0 answers

