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.
10 Likes
Hi,
Welcome. I started a thread here: Zulip
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
1 Like