[dpratt71]

If you have a goal of being able to confidently reason about your code, such as to be confident it won't go "wrong", then making it more math like would seem to make a lot of sense.

As far as the IO thing is concerned, one could use pure functions to construct a model of an imperative program. Then you just need something to run it... There is a sense in which this is exactly what is done in practice.

[AnimalMuppet]

> If you have a goal of being able to confidently reason about your code, such as to be confident it won't go "wrong", then making it more math like would seem to make a lot of sense.

Is it easier to reason about a 10,000-line-long math proof, or a 10,000-line-long program? I'm not sure that the math is actually easier.

Is it easier to write a fully-correct 10,000-line-long math proof, or a 10,000-line-long program? Again, I'm not sure that the math is actually easier.

Is it easier to write a formal prover for the math? Almost certainly. And maybe, with a formal prover, writing the correct math is easier...

[mrkeen]

> Is it easier to reason about a 10,000-line-long math proof, or a 10,000-line-long program? I'm not sure that the math is actually easier.

Don't compare them on the basis of familiarity. Making your programming language look mathy is not the point.

I'd offer a different comparison:

Reason about a 10,000-line-long math proof, or a 10,000-line-long math proof in which there are instructions to jump back-and-forth with your pencil, crossing out and updating previously-calculated values in-place.

[foobarchu]

You don't do a single proof of the entire 10k line program, you do proofs of the many small functions that make it up. If you can use each proof as an axiom going into proving the functions that use it, then each of them becomes easier to prove too. If I have a function that might sometimes mutate a variable off in another part of the program, that's just inherently harder to reason about that one that is idempotent and guaranteed to have no side effects.

[garethrowlands]

The most common proofs are those that the compiler constructs while type checking. The compiled program is the proof witness. All compilers can be thought of as producing a proof-by-construction but they vary wildly in the propositions they can prove.

If this idea is new to you and you want to learn more, google "propositions as types" or "the curry howard correspondance".