Are there Julia operational semantics available?

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:

3 Likes

In short, no. Subtyping has been formalized here, but there’s significantly more to the langauge than that.

5 Likes

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.

4 Likes

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. 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.

8 Likes

Hi,

Welcome. I started a thread here: 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: JuliaLang

1 Like