miniblog.

← Back to all posts

Wilfred Hughes

Apr 26, 2018 at 18:06

Enlightening article trying to verify leftpad (+2 other small functions) in a range of theorem provers: https://www.hillelwayne.com/post/theorem-prover-showdown/

The Great Theorem Prover Showdown

Functional programming and immutability are hot right now. On one hand, this is pretty great as there’s lots of nice things about functional programming. On the other hand, people get a little overzealous and start claiming that imperative code is unnatural or that purity is always preferable to mutation. I think that the appropriate paradigm is heavily dependent on context, but a lot of people speak in universals. I keep hearing that it’s easier to analyze pure functional code than mutable imperative code.