\section{Future work}
\label{sec:future-work}

    In this project we established some criteria for analysis of Embedded Domain-Specific Languages
    (EDSLs) for hardware description, and performed a practical analysis of some popular EDSLs by
    building and verifying simple circuits chosen as case studies. Future work in this same research
    track could emcompass, for example, the study of different EDSLs (on higher or lower levels of
    abstraction and using different host languages), the definition of different metrics and the
    modelling of larger circuits.

    One particularly interesting line of work to be pursued would be the investigation of hardware
    EDSLs hosted on dependently-typed programming languages. From the same author of Coquet, for
    instance, there is recent work on verifiable synthesis of a lightweight EDSL hosted in
    Coq~\cite{braibant2013formal}. Also, it would be interesting to investigate hardware EDSLs
    hosted in the dependently-typed programming language Agda, and which benefits they provide.

    Even in Haskell, there are already some recent developments (specially in GHC) which could be
    investigated in order to discover to which extent they might help solve the shortcomings of Lava
    and ForSyDe mentioned throughout this report. The applicability to hardware description of
    extensions such as multi-parameter type classes, data and type families, datatype promotion and
    kind polymorphism could all be studied in future work.

