conclusion.tex

\section{Conclusion}
\label{sec:conclusion}

\begin{quote}
    \emph{Nothing will ever be attempted if all possible objections must first be overcome.} 
    \begin{flushright}-- Samuel Johnson\end{flushright}
\end{quote}

Programming is increasingly a live collaboration between human programmers and sophisticated semantic services. These services need to be able to reason throughout the programming process, not just when the program is formally complete. This paper lays down rigorous type-theoretic foundations for doing just that. Bidirectional type checking helps make the localization decisions we make systematic and predictable, and type hole inference shows how local and constraint-based type inference might operate hand-in-hand, rather than as alternatives. Throughout, we focused on maintaining neutrality about user intent whenever possible. 
We hope that language designers will use the techniques introduced in this paper to consider more rigorously, perhaps even formally, the problems of type error localization and error recovery when designing future languages. 

\section*{Data Availability Statement}
An artifact \cite{zhao2023} containing the complete formalization of the marked lambda calculus and the extensions described above, the Agda mechanization, and the implementation of Hazel including type hole inference is available.
Up-to-date versions of the formalism and mechanization may be found at \url{https://github.com/hazelgrove/error-localization-agda}.
Hazel is being actively developed---more information is available at \url{https://hazel.org}, and the Hazel source code is maintained at \url{https://github.com/hazelgrove/hazel}.

\section*{Acknowledgements}
The authors would like to thank the anonymous referees at POPL 2024 and ICFP 2023 for helpful feedback on earlier drafts of this paper.
This work was partially funded through the NSF grant \#CCF-2238744.

% Thank you for reading this paper!