[mrkeen]

This may not go over as well as you'd think.

I took Haskell in the same uni course with FSAs, Turing machines, Lambda calculus, natural deduction, Hoare logic and structural induction.

So I was exposed to the "base case & step case" of structural induction at the same time as learning about it in Haskell. And for whatever reason it didn't leave a good impression. Implementing it formally was harder and more error-prone than shooting from the hip in an IDE. What was the point!?

Now I smash out Haskell code daily as the quickest way to end up with little binaries that just-work-if-they-compile. It took me a while to realise that the upside of all this formality/mathiness is that other people did the proofs so that you don't need to. I get to take for granted that a boolean is true or false (and not some brilliant third value!) and that (map f . map g) is (map (f . g)).

[edef]

> I get to take for granted that a boolean is true or false (and not some brilliant third value!)

  [True, False, undefined] :: [Bool]

[immibis]

The traditional third value is actually FileNotFound: https://thedailywtf.com/articles/what_is_truth_0x3f_

but in Haskell, yes, it's undefined. Which isn't a real value! For example, infinite loops are undefined. Theorists like to call it a value of every type, but in practical terms, it's more like a computation that never produces a value. The builtin "undefined" can be written as an infinite loop ("undefined = undefined") and many other pure infinite loops can also act as undefined values. The runtime is able to catch some and crash instead of hanging, but not others.

[mrkeen]

Nah.

  check :: Bool -> a
  check  True = undefined
  check False = undefined
  check     _ = undefined


  7:1: warning: [GHC-53633] [-Woverlapping-patterns]
      Pattern match is redundant
      In an equation for ‘check’: check _ = ...
    |
  7 | check     _ = undefined
    | ^^^^^^^^^^^^^^^^^^^^^^^

[ddellacosta]

See, you can even do quantum computing very naturally in Haskell.

[AnimalMuppet]

“A man is rich in proportion to the number of things which he can afford to let alone.” ― Henry David Thoreau, Walden or, Life in the Woods

If I have to do the proof, then as you say, it's probably harder and (in many cases) more error prone than if I didn't use a proof. If the language can do it for me, and I get the lack of errors without having to do the work (and without the chance of me making the mistakes)? Yeah, now we're talking. (Yes, I am aware that I still have to design the types to fit what the program is doing.)

If a tool introduces complexity, it has to make up for it by eliminating at least that much complexity somewhere else. If it doesn't, the tool isn't worth using.

[mpweiher]

> other people did the proofs so that you don't need to.

So?

You don't need to either.

There simply is no evidence that having such proofs has any significant effect on software quality.

https://blog.metaobject.com/2014/06/the-safyness-of-static-t...