There is already one! See Malfunction [0,1]. There is an Idris and Agda backend for malfunction. [0]: https://github.com/stedolan/malfunction https://github.c

There is already one! See Malfunction [0,1]. There is an Idris and Agda backend for malfunction. [0]: https://github.com/stedolan/malfunction https://github.com/stedolan/malfunction [1]: https://www.cl.cam.ac.uk/~sd601/papers/malfunction.pdf https://www.cl.cam.ac.uk/~sd601/papers/malfunction.pdf