Formal Logic Undressed: The Screencast

 

On September 21st of this year, I led a workshop on formal logic at the Scala World conference in the beautiful Lake District of England. Although everyone was very kind about it, I completely failed to manage my time adequately, and essentially the last third of the workshop was therefore rushed and probably rendered nearly incomprehensible. So I decided to recreate the workshop as a screencast. It might appeal to those of you who are interested in logic, especially interactive development of proofs with automated tools, as well as to a philosopher or two, and to computer programmers who are curious about the relationship between programming and logic.

The really ambitious are encouraged to install Coq and PeaCoq and follow along at home. :-)

There are 18 comments.

Become a member to join the conversation. Or sign in if you're already a member.
  1. RightAngles Member
    RightAngles
    @RightAngles

    That’s very impressive! (I don’t understand much of it ha)

    • #1
  2. Great Ghost of Gödel Member
    Great Ghost of Gödel
    @GreatGhostofGodel

    RightAngles:That’s very impressive! (I don’t understand much of it ha)

    Thanks! Logic is, I think, the ultimate in learn-by-doing, and what’s particularly nice is there are high-quality free tools like Coq and PeaCoq to take advantage of. Short of using an automated proof assistant, though, you can simply take pencil and paper in hand and do the exercises in Logical Labyrinths (half puzzle book, half textbook) or any of Smullyan’s other books.

    • #2
  3. RightAngles Member
    RightAngles
    @RightAngles

    Great Ghost of Gödel:

    RightAngles:That’s very impressive! (I don’t understand much of it ha)

    Thanks! Logic is, I think, the ultimate in learn-by-doing, and what’s particularly nice is there are high-quality free tools like Coq and PeaCoq to take advantage of. Short of using an automated proof assistant, though, you can simply take pencil and paper in hand and do the exercises in Logical Labyrinths (half puzzle book, half textbook) or any of Smullyan’s other books.

    Thank you for this! This book sounds really interesting. My only acquaintance with logic is from the aspect of philosophy in college. I know the usual stereotype of women’s thinking is that we’re illogical, and I’m pretty good at being illogical. I admire people who are good at things I’m not good at. (That means YOU)

    • #3
  4. Barkha Herman Member
    Barkha Herman
    @BarkhaHerman

    Love it!  Free Co-Yoneda indeed!

    • #4
  5. Great Ghost of Gödel Member
    Great Ghost of Gödel
    @GreatGhostofGodel

    Barkha Herman:Love it! Free Co-Yoneda indeed!

    To put some meat on those bones, please see Rob Norris’ wonderful Programs As Values presentation.

    • #5
  6. Barkha Herman Member
    Barkha Herman
    @BarkhaHerman

    For beginners (to monads)…

    • #6
  7. Great Ghost of Gödel Member
    Great Ghost of Gödel
    @GreatGhostofGodel

    See also my friend and colleague Rúnar Bjarnason’s Compositional Application Architecture With Reasonably Priced Monads.

    • #7
  8. Great Ghost of Gödel Member
    Great Ghost of Gödel
    @GreatGhostofGodel

    By the way, you can buy your very own Free the Coyoneda 10 t-shirt!

    • #8
  9. RightAngles Member
    RightAngles
    @RightAngles

    Great Ghost of Gödel:By the way, you can buy your very own Free the Coyoneda 10 t-shirt!

    This would make a great Halloween costume should I decide to go as a Logical Person.

    • #9
  10. Barkha Herman Member
    Barkha Herman
    @BarkhaHerman

    RightAngles:

    Great Ghost of Gödel:By the way, you can buy your very own Free the Coyoneda 10 t-shirt!

    This would make a great Halloween costume should I decide to go as a Logical Person.

    I had a friend once go as a mailer daemon.

    • #10
  11. RightAngles Member
    RightAngles
    @RightAngles

    Barkha Herman:

    RightAngles:

    Great Ghost of Gödel:By the way, you can buy your very own Free the Coyoneda 10 t-shirt!

    This would make a great Halloween costume should I decide to go as a Logical Person.

    I had a friend once go as a mailer daemon.

    hahaha! I can just imagine!

    • #11
  12. RightAngles Member
    RightAngles
    @RightAngles

    Great Ghost of Gödel:By the way, you can buy your very own Free the Coyoneda 10 t-shirt!

    These are good-looking and well designed.

    • #12
  13. Great Ghost of Gödel Member
    Great Ghost of Gödel
    @GreatGhostofGodel

    RightAngles:

    Great Ghost of Gödel:By the way, you can buy your very own Free the Coyoneda 10 t-shirt!

    These are good-looking and well designed.

    Thanks! I’ll tell my wife!

    • #13
  14. James Gawron Thatcher
    James Gawron
    @JamesGawron

    GGofG,

    I searched for strippers who understood Peano Arithmetic but couldn’t find any. So this is the best I could do.

    Regards,

    Jim

    • #14
  15. Great Ghost of Gödel Member
    Great Ghost of Gödel
    @GreatGhostofGodel

    James Gawron:GGofG,

    I searched for strippers who understood Peano Arithmetic but couldn’t find any. So this is the best I could do.

    Lehrer is always good for piano arithmetic! Strippers more for penile arithmetic, at which they are experts.

    • #15
  16. Underwood Member
    Underwood
    @Underwood

    Do you know the people behind the nand2tetris project?

    I noticed it on Coursera several weeks ago. It looks very interesting, but there are no future sessions scheduled. Did the initial session fail to generate much interest?

    • #16
  17. Great Ghost of Gödel Member
    Great Ghost of Gödel
    @GreatGhostofGodel

    Underwood:Do you know the people behind the nand2tetris project?

    I noticed it on Coursera several weeks ago. It looks very interesting, but there are no future sessions scheduled. Did the initial session fail to generate much interest?

    I don’t know them, but the book and software platform are complete, and obviously they have their regular teaching duties, so my guess is they just lack time. I’ve never taken a MOOC course—to be perfectly frank, they move far too slowly for me, and the social aspect is a liability rather than an asset; give me a textbook, a computer, and some coffee and I’m good, thanks—so it’s hard for me to interpret that as a loss. But other people’s learning style is different from mine, so I encourage you to contact the professors or try to find other collaborators who have gone, or are going, or would like to go through the materials.

    • #17
  18. Underwood Member
    Underwood
    @Underwood

    Great Ghost of Gödel:

    Underwood:Do you know the people behind the nand2tetris project?

    […]

    I don’t know them, but the book and software platform are complete, and obviously they have their regular teaching duties, so my guess is they just lack time. I’ve never taken a MOOC course—to be perfectly frank, they move far too slowly for me, and the social aspect is a liability rather than an asset; give me a textbook, a computer, and some coffee and I’m good, thanks—so it’s hard for me to interpret that as a loss. But other people’s learning style is different from mine, so I encourage you to contact the professors or try to find other collaborators who have gone, or are going, or would like to go through the materials.

    Thanks for the reply. The chapters for the second half of the course have not been put online, so I suspect they haven’t gotten through one cycle yet. Happily, the textbook is quite inexpensive as textbooks go.

    I haven’t taken a MOOC either. I too doubt the value of the social aspect other than the opportunity to see how others solve the same set of problems; however, I think there might be some value in having someone else (presumably with more experience and insight) evaluate one’s work, so I’ve been keeping an eye out for something suitable to try.

    • #18

Comments are closed because this post is more than six months old. Please write a new post if you would like to continue this conversation.