Correctness is Demanding, Performance is Frustrating
<|reference_start|>Correctness is Demanding, Performance is Frustrating: 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.<|reference_end|>
@article{sinkarovs2024correctness,
    title={Correctness is Demanding, Performance is Frustrating},
    author={Artjoms Sinkarovs and Thomas Koopman and Sven-Bodo Scholz},
    journal={arXiv preprint arXiv:2406.10405},
    year={2024},
    archivePrefix={arXiv},
    eprint={2406.10405},
    primaryClass={cs.PL}
}