conclusions.tex

%!TEX root = ./main.tex
\section{Conclusion}
\label{sec:conclusion}

We have presented \gcoql, the first mechanized formalization of \gql, 
implemented in the \coq proof assistant. 
% We formalize a considerable portion\td{Missing things} 
\gcoql currently covers most of the schema definition DSL, the query definition language, validity checking, and the query semantics over a graph data model. We study the query transformation proposed and exploited by Hartig and P{\'e}rez to establish their complexity results. Specifically, we provide an algorithmic definition of query normalization, proving it correct and semantics preserving. In the process we uncover and address some minor issues in the original definitions.

This work is a first step towards a mechanization of all of \gql, leaving several open venues for future work. The most pressing are supporting mutation, directives and non-null types, and experimenting with extraction in order to (ideally) derive a reference implementation directly from the mechanized specifications. We anticipate that extending \gcoql to support new features should be fairly straightforward. More engineering work needs to be done to adequately prepare the \coq development for such extensions, in particular through better modularity and automation.
% . In particular, this means that existent proofs should 
% not be easily broken or they should be easily fixable. In order to do so, it is necessary to modularize and improve the current state of tactics used in
% our proofs.
% By following a similar approach as in~\cite{empiricalgql}, one could identify key features to be included in future releases.
% \paragraph{Extending \gcoql} The current implementation does not include some features such as 
% \paragraph{Automation} 
% \paragraph{Extraction \& Testing} 
% While the current implementation attempts to be as close as possible to the grammar and algorithmic descriptions
% given in the \spec, it can be improved by extracting it to other languages and comparing it directly to the reference implementation, following the examples of~\cite{jscert, coqr}.
% We believe that the current design decisions allow for a smooth extraction.
%
Finally, we would like to study a more abstract evaluation function that is not tied to the graph data model, which should then be derivable as a specific instance. 
% \paragraph{Data model \& Spec semantics} A new evaluation function can be implemented, such that it is closer to the \spec's and defined over any data model. 
% The current semantics over graphs can then be a particular instance of this evaluation function, after addressing the limitations of the data model (\S\ref{subsec:discussion}). 
% We believe that the main difficulty lies in faithfully representing nested list types in a graph.
% \td{As we once talked, the spec's semantics can be defined using functors. Modularizing the current semantics 
% should be quite simple tbh -- I haven't done so bc: 
% 1) I'm not entirely sure how to model functors in Coq lol (I have seen implementations, but I haven't had the time to properly use them, understand them, etc),
% 2) Still the issue with the nested list types in graphs}
% \td{Collab with GraphQL foundation/community?}