Conversation

Notices

1. Ekaitz Zárraga 👹 (ekaitz_zarraga@mastodon.social)'s status on Sunday, 02-Jan-2022 16:39:22 UTC Ekaitz Zárraga 👹

   • Suguivy

   @suguivy how does this relate to Coq and stuff like that?

   • Santa Claes 🇸🇪🇭🇰🎅 repeated this.
   • Suguivy (suguivy@fedi.fai.st)'s status on Sunday, 02-Jan-2022 16:39:19 UTC Suguivy

     in reply to

     @ekaitz_zarraga Coq is a proof assistant, it implements a type theory called the Calculus of Inductive Constructions (I don't know how is it). But in Coq it's not that easy to see that when using it because it uses "tactics" that are like an abstraction to prove things more easily. In another languages like Agda you can see that correspondence better.

     Santa Claes 🇸🇪🇭🇰🎅 likes this.
   • Suguivy (suguivy@fedi.fai.st)'s status on Sunday, 02-Jan-2022 16:40:15 UTC Suguivy

     in reply to

     @ekaitz_zarraga If you are interested in the topic I can recommend you an interesting book, it's called "The Little Typer", from the creator of "The Little Schemer", maybe you know the book :)

     Santa Claes 🇸🇪🇭🇰🎅 likes this.
   • Santa Claes 🇸🇪🇭🇰🎅 (clacke@libranet.de)'s status on Sunday, 02-Jan-2022 16:42:25 UTC Santa Claes 🇸🇪🇭🇰🎅

     in reply to

     • Suguivy
     @suguivy @ekaitz_zarraga I find it really interesting how proof languages are growing from one end and implementation languages from the other, and they are finally meeting in the middle in things like Idris.