It looks a lot like Coq (proof assistant) with its tactics. You can automate the writing of your own program and you need to do it in hope of getting anything done. But you can also write the program yourself.
Anyway in Coq, you have two levels of authorship and it seems to work fine.
It looks a lot like Coq (proof assistant) with its tactics. You can automate the writing of your own program and you need to do it in hope of getting anything done. But you can also write the program yourself.
Anyway in Coq, you have two levels of authorship and it seems to work fine.