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:
In short, no. Subtyping has been formalized here, but there’s significantly more to the langauge than that.
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.
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.
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