+++
title = "Traces"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a5"]
forwardlinks = ["3a7"]
zettelid = "3a6"
+++

In CompCert proofs, observable behaviours are expressed as traces of
input-output events. These events correspond to external function calls
that interact with the outside environment in some way. For example,
printing to the console requires some system calls and would be
classified as calling an external function. Handling these in HLS is
still not quite clear, but it might become clearer eventually.