← Back to context Comment by 3lambda 7 hours ago Would this language be useful for implementing compilers and formally proving things about them? 2 comments 3lambda Reply dnautics 1 hour ago personally i think you should just have a separate proof language that doesn't also try to be a programming language and build a bridge between them (ideally as a compilation target). anyways im working on this with my spare opus tokens. physPop 3 hours ago yes thats the main reason, agda , coq similar ideas
dnautics 1 hour ago personally i think you should just have a separate proof language that doesn't also try to be a programming language and build a bridge between them (ideally as a compilation target). anyways im working on this with my spare opus tokens.
personally i think you should just have a separate proof language that doesn't also try to be a programming language and build a bridge between them (ideally as a compilation target). anyways im working on this with my spare opus tokens.
yes thats the main reason, agda , coq similar ideas