In this post, I will demonstrate how to run WebAssembly (Wasm) inside a MicroVM. I'll provide context first, then focus on a few selected implementation details. Wasm for Extensibility Architecture defines what parts of a system are stable and what parts are dynamic. System extensions are a prime example of dynamic components, but they raise significant security and observability…
"Why study compiler construction? Because knowing how a programming language is specified and implemented makes you a better programmer." I still remember these words, pronounced as matter-of-fact introduction to an undergrad course of compilers. Compiler engineers have come up with many useful programming techniques and representations. Today, I want to write about one such technique, an…
This continues a meditation on effects. My last post on the various meanings of effects in the discourse on programming languages (PL) did very little to show how type and effect discipline may be relevant to memory safety in programming languages. Moreover, I encountered a statement I found easy to agree to "before we talk about effects, we need to understand their semantics". This is an…
In the programming languages discourse, the word "effect" is used with different meanings. This can lead to confusion. In research, it is difficult to avoid jargon, but it comes at the price of making it more difficult to make sense of interconnected meanings programming language concepts. Effects - in more than one sense - are interesting today. The software industry is gearing up to move its…
There is still no standard, precise definition of memory safety. Here is a modest proposal. Fact. A programming language (PL) consists of a specification and implementation . The specification lays out precisely what the set of accepted programs is and how the code should behave when the program is executed. An implementation must conform to the specification and is what enables programmers to…
Today's post is a little different. Instead of delving into discussiong of formal type systems, I'd like to step back and talk generally about some aspects of linear type systems as they show up in real life. That means: programming languages and the memory safety discussion today, C++ and Rust. Disclaimer: while the content of this post is very much related to memory safety which is…
Today is a good day to recall some foundations of formal abstract machines, continuations, control and data stacks. And a good place to place to start is the CEK machine, described in Felleisen and Friedman's 1986 paper " Control operators, the SECD machine and the $\lambda$ calculus. " and Felleisen's 1987 dissertation . An abstract machine is a device and method for formally specifying…
This is the last and final part of my little study of polarized natural deduction by means of CBPV. The previous parts are "pt1. small steps" , "pt2. sums and products" , and "pt3. linear logic" . In this part, I will sum up what I find this interesting. This is going to be a bit more personal/opinionated/colored than the previous parts. Proof-theoretical semantics CBPV as polarized…
Welcome back to our study of polarized natural deduction and what CBPV has to do with it. For the previous parts of this journey, check out "pt1. small steps" and "pt2. sums and products" . What happened so far In part 1, we introduced the essential parts of call-by-push-value (CBPV): splitting types into value and computation types, with shifts between these worlds. We saw that static typing…
We are continuing our look at call-by-push-value (CBPV), natural deduction and abstract machines. Last time we looked at a bare-bones version so we could focus on $\lambda$-abstraction and application. In this part, we will only add sum and product types. In the next part we can then shift our view towards linear logic concepts and resources. Sum and Product Types We add a sum type $ \Sigma A_i $…
I have been reading up on call-by-push-value (CBPV), a variation of $\lambda$-calculus that is more fine-grained in its treatment of argument-passing. I then came across a chapter from Frank Pfenning's 2016 lecture notes on substructual logic that characterizes CBPV as polarized natural deduction. In a small series of posts, I am exploring what this means and how this relates to compilers.…
about me This is Burak Emir and you are looking at my homepage and blog. I mainly write about programming languages. I live in Zurich, Switzerland with my wife and two daughters, and work at Google as Alchemist of Happiness . My professional life started earlier, somewhere during my PhD in Martin Odersky's group at EPFL Lausanne where I worked on Scala and translating pattern matching. At…
Here are some snapshots from the journey (dblp) : Pattern Matching . Burak Emir. Object-oriented pattern matching. . Thesis, EPFL Lausanne, 2007. Burak Emir, Martin Odersky, John Williams. Matching objects with patterns. ECOOP 2007. Burak Emir, Qin Ma, Martin Odersky. Translation Correctness for First-Order Object-Oriented Pattern Matching. APLAS 2007 Constrained Generics (Universal Polymorphism)…
a fresh start I had to redo these pages. Using zola now. Rust, lean, a theme I like, mathjax. My old blog posts are still at bq9.blogspot.com . I wanted to like racket and pollen, but kept on forgetting everything absolutely everything. All I want is to keep some standalone note pages, and some posts, with math and code. Goodness. $e^{i\pi }+1=0$ trait Foo { fn foo ( & Self ) -> Bar } $$…