+++
title = "How to solve functional correctness"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["1f3"]
forwardlinks = ["3c", "1f2"]
zettelid = "1f3a"
+++

One solution to functional correctness is to write the HLS tool in Coq,
as we are doing with Vericert ([\#3c]). This provides guarantees that
assuming the C semantics ([\#1f2]) are correct, and the output semantics
are trusted, the translation can be trusted.

  [\#3c]: /zettel/3c
  [\#1f2]: /zettel/1f2