Correctness is Demanding, Performance is Frustrating

TL;DR

The paper tackles the challenge of achieving strong correctness guarantees without sacrificing performance in numerical programming by proposing a two-language workflow that couples a dependently-typed proof assistant (Agda) with high-performance backends (SaC and C). It introduces a rank-polymorphic array theory, an embedded DSL with reverse-mode automatic differentiation, and an extraction pipeline to generate optimized code for CNN-like computations. The approach enables formal specification, verification, and code generation all within a single framework, with the CNN example demonstrating that extracted C code can approach the performance of hand-written implementations (within about 20% in their experiments). This work argues that correctness and performance are not mutually exclusive when a dual-language, pipeline-centric design is used, and highlights opportunities for backend swap and optimization in practical numerical applications.

Abstract

In this paper we demonstrate a technique for developing high performance applications with strong correctness guarantees. We use a theorem prover to derive a high-level specification of the application that includes correctness invariants of our choice. After that, within the same theorem prover, we implement an extraction of the specified application into a high-performance language of our choice. Concretely, we are using Agda to specify a framework for automatic differentiation (reverse mode) that is focused on index-safe tensors. This framework comes with an optimiser for tensor expressions and the ability to translate these expressions into SaC and C. We specify a canonical convolutional neural network within the proposed framework, compute the derivatives needed for the training phase and then demonstrate that the generated code matches the performance of hand-written code when running on a multi-core machine.