hobbes, Morgan Stanley OSS

Over the last few years, I have been developing hobbes -- a programming language, JIT compiler, and database system -- as part of my work for Morgan Stanley. It has become a critical piece of infrastructure in our low-latency, high-volume trading applications, and we have decided to release the source code to the public on github (currently can be built for recent Linux and macOS platforms):

github.com/Morgan-Stanley/hobbes

The database system is a lightweight (self-contained, header-only) library used by applications to efficiently log structured (binary) data over shared memory to minimize application latency and reflect application type structure as accurately as possible in log files. We use this to record a very detailed image of application state over time, which we analyze/query out of band.

The JIT compiler can be used embedded in another application (e.g. to "hot patch" an application with very efficient, precisely typed intercepts) or as a standalone interactive interpreter (e.g.: to monitor and query application log data).

The programming language is a variant of Haskell (HM type inference, algebraic data types, qualified types / type classes) with some adjustments to help reduce boilerplate and derive very efficient machine code. For example, we use "structural" record, variant, and (iso-)recursive types to represent data as it's naturally represented in applications and can be deconstructed generically at compile time (e.g. a record can be printed if its first field can be printed and its rest can be printed, a variant can be printed if its first case can be printed and its rest cases can be printed, a recursive type can be printed if its one-step unrolling can be printed, etc).

We are actively using this on major projects, we will continue to develop this github project as we need new features, and we are interested in engaging others outside of the firm for their thoughts, feedback, and hopefully pull requests. :)

p5.js

p5.js is a JavaScript library inspired by Processing. Seems it could be a fun way to introduce non-CS types to programming. The demo is particularly well done; check it out first. The actual home of the project is here.

RustBelt: Securing the Foundations of the Rust Programming Language

RustBelt: Securing the Foundations of the Rust Programming Language by Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer:

Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust’s safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.

Rust is definitely pushing the envelope in a new direction, but there's always a little wariness around using libraries that make use of unsafe features, since "safety with performance" is a main reason people want to use Rust. So this is a great step in the right direction!

Undefined Behavior in 2017

Exhaustive review of Undefined Behaviors in C and C++ in 2017 by Pascal Cuoq and John Regehr.

Recently we’ve heard a few people imply that problems stemming from undefined behaviors (UB) in C and C++ are largely solved due to ubiquitous availability of dynamic checking tools such as ASan, UBSan, MSan, and TSan. We are here to state the obvious — that, despite the many excellent advances in tooling over the last few years, UB-related problems are far from solved — and to look at the current situation in detail.

YOW! Lambda Jam 2017: John Hughes - Why Functional Programming Matters

Why FP still matters (video)...

27 years ago I published “Why Functional Programming Matters”, a manifesto for FP–but the subject is much older than that! In this talk I’ll take a deep dive into its history, highlighting some of the classic papers of the subject, personal favourites, and some of my own work. At the end of the day, four themes emerge that characterize what I love about the subject.

The APL Idiom List

Via HN: The APL Idiom List – Alan Perlis, Spencer Rubager (1977)

Co-hygiene and quantum gravity

Co-hygiene and quantum gravity. Some light weekend reading by John Shutt.

The post starts with a dazzling proposition:

Gravity corresponds to pure function-application, and the other fundamental forces correspond to side-effects. ... quantum non-locality ("spooky action at a distance") is part of the analog to side-effects ...

I can't do it justice here, so if you're interested in John's fascinating take on the relationship between lambda calculus and quantum physics, hop on over!

Jean Sammet, Co-Designer of a Pioneering Computer Language, Dies at 89

Obituary from NY Times.

Jean Sammet, Co-Designer of a Pioneering Computer Language, Dies at 89
Jean E. Sammet, an early software engineer and a designer of COBOL, a programming language that brought computing into the business mainstream, died on May 20 in Maryland. She was 89.

....

Grace Hopper, a computer pioneer at Sperry Rand in the late 1950s, led the effort to bring computer makers together to collaborate on the new programming language. Ms. Hopper is often called the “mother of COBOL,” but she was not one of the six people, including Ms. Sammet, who designed the language — a fact Ms. Sammet rarely failed to point out. (Ms. Sammet worked for Sylvania Electric at the time.)

“I yield to no one in my admiration for Grace,” she said. “But she was not the mother, creator or developer of COBOL.”

Imperative Functional Programs that Explain their Work

Imperative Functional Programs that Explain their Work
Wilmer Ricciotti, Jan Stolarek, Roly Perera, James Cheney
submitted on arXiv on 22 May 2017

Program slicing provides explanations that illustrate how program outputs were produced from inputs. We build on an approach introduced in prior work by Perera et al., where dynamic slicing was defined for pure higher-order functional programs as a Galois connection between lattices of partial inputs and partial outputs. We extend this approach to imperative functional programs that combine higher-order programming with references and exceptions. We present proofs of correctness and optimality of our approach and a proof-of-concept implementation and experimental evaluation.

Dynamic slicing answers the following question: if I only care about these specific part of the trace of my program execution, what are the only parts of the source program that I need to look at? For example, if the output of the program is a pair, can you show me that parts of the source that impacted the computation of the first component? If a part of the code is not involved in the trace, or not in the part of the trace that you care about, it is removed from the partial code returned by slicing.

What I like about this work is that there is a very nice algebraic characterization of what slicing is (the Galois connection), that guides you in how you implement your slicing algorithm, and also serves as a specification to convince yourself that it is correct -- and "optimal", it actually removes all the program parts that are irrelevant. This characterization already existed in previous work (Functional Programs that Explain Their Work, Roly Perera, Umut Acar, James cheney, Paul Blain Levy, 2012), but it was done in a purely functional setting. It wasn't clear (to me) whether the nice formulation was restricted to this nice language, or whether the technique itself would scale to a less structured language. This paper extends it to effectful ML (mutable references and exceptions), and there it is much easier to see that it remains elegant and yet can scale to typical effectful programming languages.

The key to the algebraic characterization is to recognize two order structures, one on source program fragment, and the other on traces. Program fragments are programs with hole, and a fragment is smaller than another if it has more holes. You can think of the hole as "I don't know -- or I don't care -- what the program does in this part", so the order is "being more or less defined". Traces are also partial traces with holes, where the holes means "I don't know -- or I don't care -- what happens in this part of the trace". The double "don't know" and "don't care" nature of the ordering is essential: the Galois connection specifies a slicer (that goes from the part of a trace you care about to the parts of a program you should care about) by relating it to an evaluator (that goes from the part of the program you know about to the parts of the trace you can know about). This specification is simple because we are all familiar with what evaluators are.

Databases from finite categories

Spivak and Kent (2011). Ologs: A categorical framework for knowledge representation:

In this paper we introduce the olog, or ontology log, a category-theoretic model for knowledge representation (KR). Grounded in formal mathematics, ologs can be rigorously formulated and cross-compared in ways that other KR models (such as semantic networks) cannot. An olog is similar to a relational database schema; in fact an olog can serve as a data repository if desired. Unlike database schemas, which are generally difficult to create or modify, ologs are designed to be user-friendly enough that authoring or reconfiguring an olog is a matter of course rather than a difficult chore. It is hoped that learning to author ologs is much simpler than learning a database definition language, despite their similarity. We describe ologs carefully and illustrate with many examples. As an application we show that any primitive recursive function can be described by an olog. We also show that ologs can be aligned or connected together into a larger network using functors. The various methods of information flow and institutions can then be used to integrate local and global world-views. We finish by providing several different avenues for future research.

Ologs are essentially RDFs extended to encompass commuting diagrams, so a visual little language. The paper talks about how database schema can automatically be extracted from ologs.