[eli_gottlieb]

>I would like to challenge the assumption here: that programming (in whatever mode) can't be adequately described by mathematics.

Well, the entire lesson of the Halting Problem and Rice's Theorem is that it can't. Indeed, Haskell loves to just cut through the bullshit about math and be inconsistent: bottom inhabits every type, and Type inhabits Type (in Dependent Haskell).

No fixed mathematical system is capable of formally verifying all programs, or even all interesting programs. You always need more bits of axioms than of program if you want to prove theorems about your programs (Chaitin's principle, proved formally by Calude).

What we can say for FP is that Fast and Loose Reasoning is Morally Correct, and that if we use nicely categorical constructions, then when our programs happen to terminate at all, those nice constructions describe their behavior.

[Retra]

We don't actually need to butt into the Halting Problem or Rices Theorem, though.

Ideally, we would have proven-to-terminate non-turing complete DSLs that can be composed together to form more powerful DSLs. The problem is that we don't really know how to compose programs well, and when you demand the ability to peer into arbitrary executing code and modify it on the fly, you don't make it easier to learn how to do this.

If you were forced to use an architecture that separated things properly, you'd be forced to deal with those composition problems, rather than 'hacking' programs using a level of power that is unnecessary for the problem you hope to solve. (And you are hoping to solve a problem, not just run a program that fails to terminate.)

(I'm not arguing that this is the 'right way' to do things. It's just a way that should be considered properly.)

[AdieuToLogic]

> >I would like to challenge the assumption here: that programming (in whatever mode) can't be adequately described by mathematics.

> Well, the entire lesson of the Halting Problem and Rice's Theorem is that it can't.

And in mathematics, division by zero is undefined as well as not all differential equations have analytical solutions. Does that engender a lesson to abandon the rest of what the field provides?

> What we can say for FP is that Fast and Loose Reasoning is Morally Correct, and that if we use nicely categorical constructions, then when our programs happen to terminate at all, those nice constructions describe their behavior.

Not sure what you are trying to convey with the first "premise" you state, but I can say with certainty that everything after "and that if we use..." can be applied to just about any approach in making a program.

Structured Programming:

  If we use nicely decomposed procedures, then when our
  programs happen to terminate at all, those nice
  procedures describe their behaviour.

Object Oriented Programming:

  If we use nicely encapsulated classes, then when our
  programs happen to terminate at all, those nice objects
  describe their behaviour.

Declarative Programming:

  If we use nicely declared rules and capabilities, then
  when our programs happen to terminate at all, those
  nice declarations describe their behaviour.

And (your example quoted here):

  If we use nicely categorical constructions, then
  when our programs happen to terminate at all,
  those nice constructions describe their behavior.

[smosher_]

That's a little extreme. I think most computations are best¹ written in a way that is amenable to mathematical treatment, and most of the useful ones can be. Just because a counter-example exists doesn't mean we should give up hope.

I find constructing programs mathematically makes life easier in the common case and possible in nearly all others, unless you insist on things like proof-of-termination for programs which do not (I do not.)

1. 'best' because it gives us the means to reason about the code, and we know what kind of transformations we can perform on it, and do them abstractly without having to simulate it, potentially for infinite inputs, etc., etc. You know the drill.

[l_dopa]

That's a very strange interpretation of Rice's theorem. Just because properties of computable functions are undecidable doesn't mean they somehow "can't be described by mathematics". I'm also not sure why incompleteness is relevant here at all, unless you think describing something mathematically requires a complete formal system. In that case, we can't "describe" arithmetic "mathematically".

[eli_gottlieb]

It's not that strange. We can write all kinds of program analyses that are decidable, but which are necessarily conservative, and we end up deciding what sort of conservativeness (which side we want to err on) in different situations. What this does mean is that you can't really write a Grand Unified Formal Verification framework and get some wonder-of-wonders benefit just by switching to functional programming.

I've also spent enough time around Haskell coders to notice that the instant you give them a fresh new language feature, they will push it right out to the limits where the compiler's conservative analyses no longer work and the programmer has to manually assert that the code is correct.

Nothing will really save the programmer from having to think clearly about their own code, and most language features designed to ostensibly help do so just enable compiler-abuse at a higher level of abstraction.

[cousin_it]

That's correct in theory, but in practice I'd be very surprised to see a useful program that couldn't be verified by ZFC. The only natural way to get such programs is by encoding metamathematics, like trying to verify the consistency of ZFC itself.

[eli_gottlieb]

>That's correct in theory, but in practice I'd be very surprised to see a useful program that couldn't be verified by ZFC.

I think you do too much easy theory if you think that, if you'll excuse my saying so. A lot of the firmware code I write at work is just not going to be formally verifiable in any practical way without scrapping it and rewriting in a language built around formal verification from day one.

Besides which, a Python interpreter is a very common sort of program to write, actually, and I don't expect that you can "just" do the equivalent of `Require Import ZFC` to verify its behavior properly.

[cousin_it]

Point taken. Isn't that just a limitation of current tools, though? What stops ZFC from proving sentences about Python interpreters, or Brainfuck programs, or whatever? I'm not aware of any theoretical roadblocks, apart from the difficulty of actually writing out the proof (which is admittedly huge).

[eli_gottlieb]

>What stops ZFC from proving sentences about Python interpreters, or Brainfuck programs, or whatever?

Well, mostly a lack of writing down axioms about how these things actually work. The innate nondeterminism, imperative operating environment, and intentional behavior (in the sense that which implementation of a function you write actually matters) also give things that are, let's say, on the research frontier to reason about formally.

And then there's just the fact that ZFC isn't a very good language at all for programming with. Type theories are both proof-theoretically stronger and easier to write something at all like actually programs in.

Also, things like compilers and program analyzers are very common in "real-world" programming. They're just about the cutting edge of what we can do with formal verification today: it helps a lot that, as I understand things, when you write down an inductive type in a dependently-typed proof assistant, you are also writing down axioms (an induction principle) with which to prove theorems about it, and the dual for coinductive types. Then, between coinductive and inductive proofs that rely on either productive nontermination or eventually-terminating programs, we can write down most of what we actually want to code.

With the exception, of course, of proof assistants, where we can still only write a verified implementation of one system using a strictly stronger system. Gosh, if only someone was working on ways to tie that knot...

[DalekBaldwin]

"You always need more bits of axioms than of program if you want to prove theorems about your programs."

Fascinating. Is that a quote? I've never seen it stated that way. I think something about it just clicked for me.

[eli_gottlieb]

It's a paraphrase rather than a quote, of "the theorems of a finitely-specified theory cannot be significantly more complex than the theory itself."

http://www.sciencedirect.com/science/article/pii/S0196885804...

[eru]

For most tasks we can restrict ourselves to a terminating subset without bottom. See Agda, Coq, Isabelle, etc.

[eli_gottlieb]

Bingo. But most people also like to kvetch and moan about the restrictions imposed by programming with only structural recursion and productive corecursion -- even though those are usually exactly what we want.

[eru]

Especially if you get an easy way out for when you need it.

Like unsafePerformIO, but for calling not-proven-to-be-terminating functions. Or an explicit marker like the wrapping monads for side-effecting functions.

[dragonwriter]

> For most tasks we can restrict ourselves to a terminating subset without bottom. See Agda, Coq, Isabelle, etc.

While those are interesting languages, I kind of was under the impression that they were generally not seen as suitable for "most tasks".

[eru]

I mean, even in Haskell, big chunks of every program can be automatically recognized as `safe Haskell'.