Haskell for Imperative Programmers #40 - Termination Proofs

This video is supported by translatebox.io
Further reading:
www.springer.com/de/book/9783...
en.wikipedia.org/wiki/Termina...
en.wikipedia.org/wiki/Total_f...
Timestamps:
00:00 - Intro
01:06 - Non-Termination and Undefinedness
03:07 - What is Termination?
05:54 - Definition for Termination Proofs
07:09 - Factorial Proof
10:04 - Second Proof
12:36 - Precondition Correctness
14:37 - Final Thoughts

[@alexanderskusnov5119]

Did you mean 'else func' instead of 'else f' at the beginning?

[@philipphagenlocher]

Whoops... Yes, I did. Thank you for spotting that!

[@avrilianbriliansyah5290]

I somehow really like watching videos that make me feel stupid. Thank you for the video

[@philipphagenlocher]

Hehe, no problem! :P Thanks for watching!

[@Fanaro]

The "for now, that is everything" end-phrase is really catchy and unexpectedly pleasant, after hearing it a lot of times.

[@EidosGaming]

Wonderful content, keep going 😀

[@FelipeBalbi]

I got a hint of Calculus of Constructions and was wondering if you were building it up towards Coq (or another Proof assistant). Nice video

[@philipphagenlocher]

It's not going to be Coq, but another proof assistant that takes some inspiration from Haskell in its design!

[@janat234]

Can you do web dev videos about effects or aeson.

[@Fanaro]

Please use dark background for future videos, it would be nice as a change, and it would help in not blinding the viewer, though I agree this can be a personal choice.