Interesting. I didn't notice any reference to Idris [1] but that was the first place I saw this style of development.

[1] https://www.youtube.com/watch?v=mOtKD7ml0NU