<commit_before>\section{Introduction}
\label{sec:introduction}

\lee{Lee will take a stab at this. The main point of this paper is that there
  has been a long history of ``safe C'' languages that involved building new
  compilers. They allow low-level programming while ensuring type-safety. We
  show that with a modest set of generic type-level features, such a language
  can be built as an EDSL in which the safe-C type system is embedded in
  Haskell's type system, with a small number of exceptions. We'll also talk
  about some of the benefits and detriments of a safe C EDSL as opposed to a
  stand-alone compiler. In some sense, this is a follow-up to Stephanie's ICFP
  keynote showing what you can do with Haskell's dependent types (meaning
  decidable type inference in our usage).}

In 2014, we published an experience report describing our approach to building
high-assurance embedded systems, particularly focused on the use of
EDSLs~\cite{smaccm}. In that paper, we briefly introduced a language called
\emph{Ivory} for programming high-assurance embedded systems. While we briefly
discussed our user experience of Ivory there. Our main application with the
language has been to write \emph{SMACCMPilot}, a full-featured autopilot for a
small unpiloted air vehicle that was the subject of a ``penetration test'' by
the U.S. Government. Here we describe the design and implementation of the
language.

Ivory follows in the footsteps of other ``safe C'' programming languages, such
as Cyclone~\cite{}, Rust~\cite{}, \lee{others?}. By safe C languages, we mean
languages that avoid many of the pitfalls of C, particularly related to memory
safety and undefined behavior, that are suitable for writing low-level code
(e.g., device drivers), and that provide low-level control over timing behavior
and memory usage. Ivory, like other safe C languages, has a minimal runtime
system.

\paragraph{Contributions}
In 2014, <NAME> gave a keynote address at the International
Conference on Functional Programming describing dependent programming using the
type-extensions of GHC's implementation of Haskell (which we will colloquially
refer to as ``GHC'' in the remainder of this
paper)~\cite{weirich-keynote}. Weirich describes how recent extensions to GHC
provide much of the power of dependently-typed programming, such as found in
Agda~\cite{}, Idris~\cite{}, or Coq~\cite{}. However, in GHC, a surprisingly
powerful subset of dependent typing features can be used while still enjoying
type-inference and decidable type-checking~\cite{dephaskell}.

Ivory exemplifies the use of GHC dependent types in a large, fully-featured<commit_msg>Fix a typo<commit_after>\section{Introduction}
\label{sec:introduction}

\lee{Lee will take a stab at this. The main point of this paper is that there
  has been a long history of ``safe C'' languages that involved building new
  compilers. They allow low-level programming while ensuring type-safety. We
  show that with a modest set of generic type-level features, such a language
  can be built as an EDSL in which the safe-C type system is embedded in
  Haskell's type system, with a small number of exceptions. We'll also talk
  about some of the benefits and detriments of a safe C EDSL as opposed to a
  stand-alone compiler. In some sense, this is a follow-up to Stephanie's ICFP
  keynote showing what you can do with Haskell's dependent types (meaning
  decidable type inference in our usage).}

In 2014, we published an experience report describing our approach to building
high-assurance embedded systems, particularly focused on the use of
EDSLs~\cite{smaccm}. In that paper, we briefly introduced a language called
\emph{Ivory} for programming high-assurance embedded systems. While we briefly
discussed our user experience of Ivory there, our main application with the
language has been to write \emph{SMACCMPilot}, a full-featured autopilot for a
small unpiloted air vehicle that was the subject of a ``penetration test'' by
the U.S. Government. Here we describe the design and implementation of the
language.

Ivory follows in the footsteps of other ``safe C'' programming languages, such
as Cyclone~\cite{}, Rust~\cite{}, \lee{others?}. By safe C languages, we mean
languages that avoid many of the pitfalls of C, particularly related to memory
safety and undefined behavior, that are suitable for writing low-level code
(e.g., device drivers), and that provide low-level control over timing behavior
and memory usage. Ivory, like other safe C languages, has a minimal runtime
system.

\paragraph{Contributions}
In 2014, <NAME> gave a keynote address at the International
Conference on Functional Programming describing dependent programming using the
type-extensions of GHC's implementation of Haskell (which we will colloquially
refer to as ``GHC'' in the remainder of this
paper)~\cite{weirich-keynote}. Weirich describes how recent extensions to GHC
provide much of the power of dependently-typed programming, such as found in
Agda~\cite{}, Idris~\cite{}, or Coq~\cite{}. However, in GHC, a surprisingly
powerful subset of dependent typing features can be used while still enjoying
type-inference and decidable type-checking~\cite{dephaskell}.

Ivory exemplifies the use of GHC dependent types in a large, fully-featured
{'fraction_non_alphanumeric': 0.05636466805371666, 'fraction_numerical': 0.0030262909022129754, 'mean_word_length': 4.785557986870897, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '314608', 'n_tokens_mistral': 1404, 'n_tokens_neox': 1323, 'n_words': 763}