> In the general-purpose programming context, imagine if you could give examples of a program output (domain data) along with a skeleton of a program (source fi

> In the general-purpose programming context, imagine if you could give examples of a program output (domain data) along with a skeleton of a program (source file with incomplete parts) and ask a system to fill in the holes. This part reminds me of some of capabilities of the Idris compiler [1]. In an Idris program you can leave "holes" to stand in for incomplete parts of a program [2], and the compiler can infer various bits of code from types and holes. In a demo of the in-progress Idris 2 compiler [3], Edwin Brady refers to it as a "lab assistant" and shows it writing a whole function when given a function type. [1] http://docs.idris-lang.org/en/latest/tutorial/interactive.html#editing-commands http://docs.idris-lang.org/en/latest/tutorial/interactive.ht... [2] http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#holes http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html... [3] https://www.youtube.com/watch?v=mOtKD7ml0NU https://www.youtube.com/watch?v=mOtKD7ml0NU