Provably trustworthy systems

We present recent work on building and scaling trustworthy systems with formal, machine-checkable proof from the ground up, including the operating system kernel, at the level of binary machine code. We first give a brief overview of the seL4 microkernel verification and how it can be used to build verified systems. We then show two complementary techniques for scaling these methods to larger systems: proof engineering, to estimate verification effort; and code/proof co-generation, for scalable development of provably trustworthy applications. This article is part of the themed issue ‘Verified trustworthy software systems’.

ARTIFICIAL SEISMIC SHADOW ZONE BY ACOUSTIC METAMATERIALS

We developed a new method of earthquake-proof engineering to create an artificial seismic shadow zone using acoustic metamaterials. By designing huge empty boxes with a few side-holes corresponding to the resonance frequencies of seismic waves and burying them around the buildings that we want to protect, the velocity of the seismic wave becomes imaginary. The meta-barrier composed of many meta-boxes attenuates the seismic waves, which reduces the amplitude of the wave exponentially by dissipating the seismic energy. This is a mechanical method of converting the seismic energy into sound and heat. We estimated the sound level generated from a seismic wave. This method of area protection differs from the point protection of conventional seismic design, including the traditional cloaking method. The artificial seismic shadow zone is tested by computer simulation and compared with a normal barrier.

Type classes for mathematics in type theory

The introduction of first-class type classes in the Coq system calls for a re-examination of the basic interfaces used for mathematical formalisation in type theory. We present a new set of type classes for mathematics and take full advantage of their unique features to make practical a particularly flexible approach that was formerly thought to be unfeasible. Thus, we address traditional proof engineering challenges as well as new ones resulting from our ambition to build upon this development a library of constructive analysis in which any abstraction penalties inhibiting efficient computation are reduced to a minimum.The basis of our development consists of type classes representing a standard algebraic hierarchy, as well as portions of category theory and universal algebra. On this foundation, we build a set of mathematically sound abstract interfaces for different kinds of numbers, succinctly expressed using categorical language and universal algebra constructions. Strategic use of type classes lets us support these high-level theory-friendly definitions, while still enabling efficient implementations unhindered by gratuitous indirection, conversion or projection.Algebra thrives on the interplay between syntax and semantics. The Prolog-like abilities of type class instance resolution allow us to conveniently define a quote function, thus facilitating the use of reflective techniques.