Comment by 3lambda 8 hours ago Would this language be useful for implementing compilers and formally proving things about them? 2 comments 3lambda Reply dnautics 2 hours 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 5 hours ago yes thats the main reason, agda , coq similar ideas
dnautics 2 hours 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