Introduction

My general ambition is to accelerate software development. At the moment I am particularly interested in abstractions capturing the trifecta of correctness, performance, and interpretability. Some inspiring examples include the pipes streaming framework designed in the vein of applied category theory (Gonzalez 2012), Chlipala’s synthesized crypto routines (Erbsen et al. 2019), and metacompilation work with Python (Bolz and Tratt 2015) and Lua (Xu 2022). pipes’ design elegantly avoids other libraries’ unsoundness without compromising performance; Chlipala synthesizes from high-level machine-checked code a fastest-known crypto routine implementation; metatracing and metacompilation yield competitive JITs at a fraction of effort. The common thread unifying these is applying foundational theory to well-chosen areas and producing practical results outperforming prior heuristic approaches.

Experience

PL

Let me showcase my experience.

I had previously worked on a security policy to runtime monitor compiler in the vein of SELinux¹ for Kaspersky OS² (Kaspersky 2015). The project used to compile PSL the Policy Specification Language to C directly, which lead to binary blowup for large and/or complicated policies like LTL³ with regexps. Our team thus sketched out a subset of PSL in Agda and designed a simple stack IR. With this we both decoupled type elaboration from codegen (sic) and were free to implement optimization passes, reducing the binary size severalfold.

Our project was modular w.r.t. policy engines: that is, providers could be plugged into the compiler to imbue particular PSL syntax with semantics. Providers’ codegen and composition are implemented with nk-sketch⁴, a Nix-style AST build system inspired by the SKETCH synthesis tool (Solar-Lezama et al. 2006). A sketch is a template with holes that the compilation process fills (formally, a sketch is a key, a list of dependencies, and a cache of holes). Templates were written in C before the IR project, but nk-sketch is fully general.

Before joining Kaspersky, I did a research internship at Jetbrains’ MLSE⁵ lab, fuzzing the Kotlin compiler for performance; that is, to find anomalously slow-to-compile inputs. Whitebox methods were dismissed for Kotlin is complicated and lacks a formal description; blackbox neural generation with heuristic filter à la (Cummins et al. 2018) seemed viable but dumb; so I tried out AFL⁶. With instrumentation available at the time (Padhye, Lemieux, and Sen 2019), that came down⁷ to 5 \mathrm{\frac{samples}{sec \ast core}}. Prior work on domain-general semantic fuzzing (Padhye et al. 2019) didn’t work well with such slow feedback; so I tried bootstrapping from the compiler performance test suite and implementing Kotlin-specific mutators. That’s when my internship ran out, with inconclusive results. One thing I learned from that is to estimate the research-readiness of the subject: I spent an inordinate amount of time patching an unfamiliar industrial compiler having expected to work at a much higher level than that. Still, that work could further be fleshed out into a “CompilerGym”⁸ of sorts.

Networks

Prior to having pivoted to PL work, I did networks: a joint project and an independent one.

My group at eQualitie⁹ approached the censorship resistance problem from an unusual angle: in lieu of an ever-more-sophisticated DPI¹⁰-resistant proxy, we served the static Web with BitTorrent (eQualitie 2018). That let us reduce the traffic that needed to be expensively proxied and handle networks temporarily or semi-permanently separated from the global Internet (such as a country flipping the Internet switch). My particular contribution was in the distributed naming scheme we used and adjusting the P2P code to mobile clients. This work was presented as (Ivan Vilata-i-Balaguer 2019).

I got the eQualitie contract after presenting gnunet-hs (Volkov 2019) (Volkov 2018), an experiment in wrapping GNUnet (Grothoff 2017), an intimidating C P2P application runtime complete with a CPS¹¹ scheduler, into a simple imperative Haskell API. This was engineering and API design work directed to lowering the barrier to P2P application development and raising the exposure of a productive Haskell+C PL combination (Volkov 2020), culminating in a port of Cloud Haskell¹² (Epstein, Black, and Peyton-Jones 2011) to GNUnet’s CADET¹³.

An anecdote: upon reading the Jitk (Wang et al. 2014) and Firecracker (Agache et al. 2020) papers back in 2020 – briefly, Jitk runs a Coq→OCaml extracted BPF JIT in userspace; kernel downcalls to it; Firecracker is a lightweight virtualization system powering AWS Lambda – I had the idea of running a BPF VM as a unikernel with virtio network as an alternative to the likes of DPDK and prototyped¹⁴ this up to virtio-net initialization in baremetal Rust before life intervened. I imagine grad school is where life doesn’t intervene so.

PLV outreach

Besides that, my teaching experience totals ca. 400 hours, most of that intensive instruction in functional programming and distributed systems at summer schools, both to students and seasoned software engineers. In 2021 I organized Lalambda, a two-week summer school on formal methods hosting 70 participants in collaboration with Anton Trunov.

Research interests

As stated earlier, I aspire to do applied theoretic work yielding correct and performant artifacts. Particular areas I find curious are gradual typing, program synthesis and extensible compilation, and specification logics. Some particular ideas follow:

Static typing limits expressiveness; typing statically what can be thus typed ergonomically and leaving the rest to dynamic checks (Siek and Taha 2006) is a compromise whose value is attested to by TypeScript and mypy. There is practical work to be done with these to add soundness without sacrificing performance (Rastogi et al. 2015). Another exciting direction is recent work in gradualizing Coq’s CIC¹⁵ (Lennon-Bertrand et al. 2022); this suggests a new sort of proof assistants and dependently-typed languages and is very curious.

Synthesis and extensible compilation both make code easier to reason about and verify, faster to develop, and offer very real performance gains – as evidenced by Halide and Exo. I am particularly interested in verified synthesis with the Fiat (Delaware et al. 2015) refinement framework, and further Fiat-to-Facade and the Rupicola relational compiler. These are ripe for application to further targets (like synthesizing an SMT solver) and development of the corresponding theory.

On the other hand, some systems are intractable to synthesize: prominently, DNN control systems. One avenue is furthering simulation; another is to scale direct verification of DNNs via SMT solvers (Katz et al. 2021), in particular reducing case-splitting by better conflict prediction, or providing better soundness guarantees by extending Barrett’s work (Katz et al. 2016) to support the full input language of CVC4.

Iris¹⁶’s (Jung et al. 2015) success suggests the right logic can be tremendously valuable to reason about a wide range of domains from weak memory models (Mével and Jourdan 2021) to CRDTs¹⁷ (Nieto et al. 2022) to OCAPs¹⁸ (Swasey, Garg, and Dreyer 2017), and even build executable specifications of distributed systems (Krogh-Jespersen et al. 2020) (Hawblitzel et al. 2015). Clearly, there is no shortage of research to be done here; one exciting problem is generalizing Simuliris’s (Gäher et al. 2022) results from a particular program transformation to general optimizations or adapting it to a weak memory model.

For another direction, staged compilation seems to be the next evolution step of domain-specific metaprogramming systems like FFTW, ATLAS, or Halide (Kiselyov 2018) and further makes some styles of program analysis and synthesis more viable as evidenced by recent work in staged abstract and relational interpreters (Wei, Chen, and Rompf 2019). One imagines extending that work to richer languages, such as higher-order ones.

Finally, I feel putting engineering effort into tooling (c.f. Proof General, Alectryon, Dotty decompiler) can improve many an academic’s research or teaching experience.

One comparative advantage I bring to the table is six years’ worth of systems experience. That means I’m proficient with pushing out code; what I’m looking for is a mentor to guide my research and an org process optimized for crystallizing and publishing quality ideas.

References