Alexi
Turcotte,
Master’s
candidate
David
R.
Cheriton
School
of
Computer
Science
Foreign function interfaces (FFIs) are commonly used as a way to mix languages together. In such systems, a program written in a host language calls functions written in a guest language from within the same program. Perhaps the most popular language to interface with is C, due in no small part to its performance, and it's not uncommon for programmers to write performance-critical code in C and call it from other languages. But while C is a very performant language, it is far from being memory-safe, and one might expect C to introduce unsoundness into host language systems.
This host/guest language relationship echoes that of typed and untyped code in gradual type systems. In such systems, untyped values flowing into typed code must be cast at the boundary between typed and untyped code, and this introduces the possibility for runtime type errors in otherwise statically guaranteed code. Similarly, when a host language calls a function written in a guest language, this introduces any unsoundness in the guest language to the host language, and new errors become possible at runtime.
In this thesis, we explore the effects of C on languages using a C FFI. To demonstrate, we give a formalization of Poseidon Lua, an environment wherein Typed Lua code may call C functions, cast C values, and allocate C data. To showcase the interaction between Lua and C, we choose to formalize a core calculus for Lua, and do not model C per se; instead, we reason about C as if C calls were a black-box, remaining general with respect to C's semantics, while carefully quantifying the effects that C can have on Lua by leveraging the concept of blame from gradual typing. We present a nondeterministic operation semantics for Poseidon Lua, and use blame to assure that C is always at fault for runtime errors in Lua.