blob: 65ebc428c90735d8cfe9deb09095270a7142a5bd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
+++
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
|
