Haskell for Imperative Programmers #39 - Induction Proofs

This video is supported by translatebox.io
Further reading:
en.wikipedia.org/wiki/Well-fo...
en.wikipedia.org/wiki/Ascendi...
en.wikipedia.org/wiki/Structu...
Timestamps:
00:00 - Intro
02:18 - The Induction
02:54 - Noetherian Induction
03:55 - Structural Induction
05:36 - Example of structural induction
07:12 - Problems with our proof
08:09 - Computation Induction
10:43 - Example of computation induction
12:34 - A bit of discussion

[@ashwinmathi8042]

“Sum what formally proven”
A joke as elegant as this series. Thank you so much

[@FelipeBalbi]

Enabling notifications because I don't want to miss the Proof Assistant video :-) Nice work, Philipp. Cheers

[@philipphagenlocher]

That's the spirit! ;D

[@johnmathgood4184]

Same, I’ve been waiting for this

[@griof]

Great you got an sponsor!

[@magnusdominus2866]

Great content king! Glad to see you again

[@wolfinthesuit]

Man that's why Haskell is harder than python

[@user-ux2kk5vp7m]

How does this not apply to python?

[@VinyZikss]

haskell is a pain in the ass, thats what

[@user-ux2kk5vp7m]

@@VinyZikss you did not answer my question

[@wolfinthesuit]

@@VinyZikss agreed