# Would it make sense for Julia to adopt refinement types?

**URL:** <https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586>\
**Category:** Internals & Design\
**Created:** [April 28, 2024, 1:38pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586 "2024-04-28T13:38:08Z")\
**Posts on this page:** 1\
**Showing post:** 8

<div class="post-metadata">

**Author:** ![mefob](https://avatars.discourse-cdn.com/v4/letter/m/ea5d25/32.png) [@mefob](https://discourse.julialang.org/u/mefob)\
**Post date:** [May 7, 2024, 4:19am UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/8 "2024-05-07T04:19:14Z")

</div>

I would love to see refinement types myself. Having tinkered with Ada/SPARK in the past, I am convinced this is great and straightforward way to avoid many bugs.

Once the annotations are in place, a lot can be done to improve program quality, from injecting dynamic tests, to a full formal verification of the entire program.

It is not clear if there is a single best approach, probably a mix of different approaches is best.

As a first step, we’d need a way to attach additional specifications to variables or return values of functions, such as

- range
- set membership
- arbitrary predicates

I don’t think there is currently a way to add attributes to variables, but the user-facing syntax could look like this:  
`@annotation 0 < x < 10`  
`@annotation myPredicate(x) == true`  
The annotations could also go into docstrings:

```julia
"""
N counts the 
@annotation n > 0
"""
n::Integer

```

Based on these annotations, libraries could generate tests, add dynamic checks, or try to statically prove the assertions.

Such checks would not have to be part of the core, different verification tools could use different approaches. As an example, one tool could verify ranges, while another tool could verify physical units.

Some libraries to study for inspiration:

> **[“learn.adacore.com"](https://learn.adacore.com/courses/intro-to-spark/index.html)**
>
> An interactive learning platform to teach the Ada and SPARK programming languages.

[https://docs.adacore.com/spark2014-docs/html/ug/en/source/type\_contracts.html#predicates](https://docs.adacore.com/spark2014-docs/html/ug/en/source/type_contracts.html#predicates)

> <https://github.com/creusot-rs/creusot/blob/master/ARCHITECTURE.md>

These annotations could also be used, very naturally, to implement design by contract:

> [@DesignByContract.jl: DbC interface for Julia (feedback)](https://discourse.julialang.org/t/designbycontract-jl-dbc-interface-for-julia-feedback/49079):
>
> I’ve been working on a new package for Julia which brings the “Design by Contract” functionality from Eiffel in the form of macros. I think this is something that could be used on future Julia application development, when considering the correctness checks on runtime as well as easing the testing process. However, developing a package that is basically adding checks embedded within Julia code seems a bit off since the language thrives on efficiency. I wanted to know the community’s thoughts on…

[https://www.cs.cmu.edu/~csd-phd-blog/2023/rust-verification-with-verus/](https://www.cs.cmu.edu/~csd-phd-blog/2023/rust-verification-with-verus/)

> **[GitHub - newca12/awesome-rust-formalized-reasoning: An exhaustive list of all...](https://github.com/newca12/awesome-rust-formalized-reasoning)**
>
> An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification. - newca12/aw...

Variable annotations would also nicely enable design by contract

> [@DesignByContract.jl: DbC interface for Julia (feedback)](https://discourse.julialang.org/t/designbycontract-jl-dbc-interface-for-julia-feedback/49079):
>
> I’ve been working on a new package for Julia which brings the “Design by Contract” functionality from Eiffel in the form of macros. I think this is something that could be used on future Julia application development, when considering the correctness checks on runtime as well as easing the testing process. However, developing a package that is basically adding checks embedded within Julia code seems a bit off since the language thrives on efficiency. I wanted to know the community’s thoughts on…

Additionally, they would also be useful for physical units, e.g. through Unitful.jl.

---

_[View the full topic](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586)._