# A Coq-based synthesis of Scala programs which are correct-by-construction

## TL;DR

This paper presents Scala-of-Coq, a compiler enabling the synthesis of correct-by-construction Scala programs from Coq specifications, facilitating seamless integration into industrial applications.

## Contribution

It introduces Scala-of-Coq, a novel compiler that synthesizes Scala programs from Coq proofs, ensuring correctness by construction.

## Key findings

- Successfully synthesizes Scala programs from Coq specifications
- Ensures correctness-by-construction in generated code
- Facilitates integration into existing Scala/Java applications

## Abstract

The present paper introduces Scala-of-Coq, a new compiler that allows a Coq-based synthesis of Scala programs which are "correct-by-construction". A typical workflow features a user implementing a Coq functional program, proving this program's correctness with regards to its specification and making use of Scala-of-Coq to synthesize a Scala program that can seamlessly be integrated into an existing industrial Scala or Java application.