Show HN: Dependently typed language for proofs that you can implement in one day

Re:Show HN: Dependently typed language for proofs that you c... by baddash on Saturday October 02, 2021 @04:13AM (#28726944)

So, as someone who is curious but have no idea of the theoretical background here.. what should I learn in order to help me understand the code + use this language in a basic way? I think the idea of being able to construct proofs is pretty cool but I'm pretty lost here.

[ Parent | on HN ]

Re:Show HN: Dependently typed language for proofs that you c... by evolveyourmind on Saturday October 02, 2021 @04:19AM (#28726970)

If you want to learn more about the basics of theorem proving through dependent types, Wadler’s Agda tutorial at https://plfa.github.io would be a good starting point

[ Parent | on HN ]

Re:Show HN: Dependently typed language for proofs that you c... by baddash on Saturday October 02, 2021 @04:29AM (#28727024)

appreciate it, thanks

[ Parent | on HN ]

Re:Show HN: Dependently typed language for proofs that you c... by caotic123 on Saturday October 02, 2021 @04:55AM (#28727135)

I also recommend the software foundations in coq https://softwarefoundations.cis.upenn.edu/.

[ Parent | on HN ]