Sure, but as of July 2015 the programming languages (e.g. Agda, Idris) that can ...

mafribe on July 6, 2015 | parent | context | favorite | on: New Paper: Theory of Programs

Sure, but as of July 2015 the programming languages (e.g. Agda, Idris) that can give full specifications of their own programms, are experimental, not mainstream.