Functional Compiler Engineer
About Heliax
Heliax is a remote-first public goods lab which researches, develops, deploys, and maintains open-source protocols & mechanisms designed to serve the everyday needs of humanity. Using this, we build vertically integrated open-source products and networks that form coherent open systems which are capable of acting as an alternative to existing exploitative paradigms. With team members located around the world, our work culture is characterized by open-allocation, where team members have a high degree of freedom and autonomy in choosing when to work, what to work on, and whom to work with.
Heliax’ work include the Anoma protocol, a novel architecture for blockchains that enables a declarative paradigm for decentralized applications; Namada, a proof-of-stake L1 for interchain asset-agnostic privacy; Juvix and Vamp-IR, in the domain of languages for dApps and ZK circuits.
Overview
Smart contracts are not secure enough for finance, law, or systems engineering.
Heliax is working on a dependently-typed smart contract language, Juvix, which utilises recent advancements in type theory to allow developers to write code in a high-level functional language, compile it to gas-efficient output VM instructions, and formally verify the safety of their contracts prior to deployment & execution.
PLT at Heliax focuses on applying the latest research in type theory and programming language design to concrete problems in the distributed ledger space. We are looking for a functional compiler engineer to work on various parts of the Juvix stack, all the way from optimising inlining heuristics in the core compiler passes to using Juvix’s granular linearity information in order to write an efficient LLVM compilation backend.
This role offers the chance to work closely with a small team on compelling cross-disciplinary problems in computer science, PLT, cryptography, and economics, and enjoy a high degree of independence in working conditions and prioritisation.
Responsibilities
- Produce formal specifications and implementation plans for new language features in collaboration with team members (and optionally submit to academic venues)
- Evaluate correctness, suitability, and ease-of-implementation of published PLT and compiler engineering research for the Juvix architecture & project aims
- Implement both in-house and published research in Haskell in the Juvix codebase in collaboration with team members
- Conduct code reviews and help maintain a high standard of correctness and quality
- Conduct benchmarks of Juvix output code and adjust both the compiler architecture and details of specific passes to optimise its performance while retaining correctness
- Comprehensively document both design and implementation choices in the codebase, and assist in writing user-facing documentation for the Juvix language
Primary Project
Qualifications
- Prior experience in functional programming in Haskell, Idris, Agda, or Coq
- Prior experience in compiler engineering, especially for a functional language
- Self-motivated & self-organised
- Interested in open-source technology and research applied to DLT
Bonus Qualifications
- Prior academic work in type theory, PLT, or compiler design
- Prior academic work in cryptography, economics, or game theory
Misc
Remote or local (Zürich/Zug, Berlin). When remote, preferred if mostly located within (+/- 7 hours) Central European time zones. Ideally someone who enjoys nature and hiking 🏔️.