# Are there Julia operational semantics available?

**URL:** <https://discourse.julialang.org/t/are-there-julia-operational-semantics-available/52923>\
**Category:** Internals & Design\
**Created:** [January 6, 2021, 9:07am UTC](https://discourse.julialang.org/t/are-there-julia-operational-semantics-available/52923 "2021-01-06T09:07:32Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![0x0f0f0f](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/0x0f0f0f/32/20806_2.png) [@0x0f0f0f](https://discourse.julialang.org/u/0x0f0f0f)\
**Post date:** [January 6, 2021, 9:07am UTC](https://discourse.julialang.org/t/are-there-julia-operational-semantics-available/52923/1 "2021-01-06T09:07:32Z")

</div>

I am interested in using Julia for my thesis. Is there any formal system backing Julia’s semantics? At least the core language? For example, in other languages:

> **[1406.2061.pdf](https://arxiv.org/pdf/1406.2061.pdf)**
>
> 224.48 KB

---

<div class="post-metadata">

**Author:** ![StefanKarpinski](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/stefankarpinski/32/24_2.png) [@StefanKarpinski](https://discourse.julialang.org/u/StefanKarpinski)\
**Post date:** [January 6, 2021, 2:25pm UTC](https://discourse.julialang.org/t/are-there-julia-operational-semantics-available/52923/2 "2021-01-06T14:25:44Z")

</div>

In short, no. Subtyping has been formalized [here](https://dl.acm.org/doi/pdf/10.1145/3276483), but there’s significantly more to the langauge than that.

---

<div class="post-metadata">

**Author:** ![thautwarm](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/thautwarm/32/37760_2.png) [@thautwarm](https://discourse.julialang.org/u/thautwarm)\
**Post date:** [January 7, 2021, 6:54pm UTC](https://discourse.julialang.org/t/are-there-julia-operational-semantics-available/52923/3 "2021-01-07T18:54:41Z")

</div>

It would be very useful to have this, which could attract a few people from certain fields or even further, contribute to the prospective verification of many Julia applications.

However it is also a heavy task(even for recognizing the appropriate core lang). The good news is the community is nice, and if you try, I believe many are willing to help you.

I for one can help review this or discuss when you have questions.

---

<div class="post-metadata">

**Author:** ![0x0f0f0f](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/0x0f0f0f/32/20806_2.png) [@0x0f0f0f](https://discourse.julialang.org/u/0x0f0f0f)\
**Post date:** [January 8, 2021, 12:20am UTC](https://discourse.julialang.org/t/are-there-julia-operational-semantics-available/52923/4 "2021-01-08T00:20:36Z")

</div>

Thanks @thautwarm @StefanKarpinski.

I’ll start working on my thesis in the next months.  
The background idea is to implement an effect system for a functional programming language, similar to [Koka](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/algeff-tr-2016-v3.pdf). Koka’s formalization helped with extensive static analysis to generate code that does not need garbage collection at runtime.

I liked Julia’s LISP-like metaprogramming features a lot, something which OCaml (the other candidate lang for my work) sort of lacks. Metaprogramming simply makes the job easier. I hope my thesis advisor considers using Julia, formalizing it is a quite hard task though, not sure if doable by a single person for a thesis project.

@thautwarm Any discourse sections where I can post a a call for collaboration?

Anyways, could a formal type system and semantic model also help with static compiling of Julia code? PackageCompiler and Fezzik or general internal issues like time to first plot?

I thought about identifying a subset of Julia, with at least a core set of mandatory type annotations, strict enough to allow approximations of the list of imports needed. This would remove the need of writing tests to trace imports in compiling a static relocatable binary with PackageCompiler. Please let me know if you think this is doable.  
Eager to contribute together to Julia. Let’s keep in touch.

---

<div class="post-metadata">

**Author:** ![Akatz](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/akatz/32/15164_2.png) [@Akatz](https://discourse.julialang.org/u/Akatz)\
**Post date:** [January 8, 2021, 12:59am UTC](https://discourse.julialang.org/t/are-there-julia-operational-semantics-available/52923/5 "2021-01-08T00:59:09Z")

</div>

Hi,

Welcome. I started a thread here: [Zulip](https://julialang.zulipchat.com/#narrow/stream/137791-general/topic/Static.20typing.20.2F.20static.20analysis.20for.20Julia/near/222022960)

For discussion of Julia + static typing and analysis and pinged people interested in the topic. Feel free to reach out!

you can join the zulip with this link: [Julia Community](https://julialang.zulipchat.com/register/)