The Great Theorem Prover Showdown
hillelwayne.com
hillelwayne.com
"..There was zero overlap between the provers and the bulldogs. I was expecting at least some overlap: somebody who mocked me but also provided a valid solution, or even tried but failed. But that didn’t happen.
I normally assume these people are “brilliant jerks”: they’re assholes online, but I still have to listen to them in case they say something important. This really cracked that assumption: none of the “brilliant jerks” were willing to put any skin in the game. You don’t have to listen if they have nothing to say."
There are many who are good at making noise and opining, and even talking about wonderful "tech" that they are working on, but most of the "brilliant jerks" ultimately produce nothing of value and contribute nothing to the ecosystem.
If you adopt the strict definition of "correct", then "more" correct makes no sense, of course.
I recently ported a fairly hairy lengthy algorithm from python to scala. From something with a ton of mutability, scope confusion, exceptions serving as GOTOs for business logic - into scala pure functions. The python was inscrutable with a team of people treating it gingerly. The scala is easily refactorable and each time we take another crack at it, it shrinks into smaller and smaller code (and not by using crazy Scala) and I suspect that much of the confusing hairy complexity will disappear. I don't really know how to quantify this, but I don't think it's captured from an exercise that compares difficulty in formally proving methods in IP and FP.
So yeah... it's an awesome exercise that showed a lot, and I really want to dig more into provers, but I just don't see that his "therefore" follows, that "it's (not) easier to reason about FP than imperative".
On the other hand, it's pretty easy to widen the scope of what you're proving correct about a program in such a way as to make it impossible for Haskell to help you. For instance, "accomplish this in O(n)" or "use less than 1 MB" or "in less than 1 second." People usually only concern themselves with the aspects of the implementation that Haskell prioritizes by surfacing as return values. But there are certainly settings where the method used is as important as getting the answer mathematically correct--in fact the rise of NoSQL shows us that there are even situations where doing the wrong thing quickly is better than aborting in the face of unrecoverable errors.
You should use domain-specific language embedded into it for that.
If you do that that way, Haskell can help you with particular details of the implementation with types (I think that O(n) would be easy - I did parametrization on the length circa 2008) and help you to connect your implementation and the rest of program, again, with types.
I did exactly that. From well-typed parsers for stream processing hardware to (not-so-well typed for historical reasons) strict realtime algorithms.
I have noticed the same thing with my Haskell code. In other languages with side effects, I often tend to write much more complicated procedures, with cross-cutting concerns. Haskell forces me to break it down more.
Maybe FP really is harder to reason about (and write), and that's why people have to write it much more clearly in more manageable chunks. But paradoxically, the net effect is positive, it's actually what makes it easier to reason about (and read) in the end. (And the separation of side effects makes a big difference here.)
> I don't really know how to quantify this
I was thinking about this. Maybe there should be some information theory framework that could capture complexity of functions (including side-effects). For example, compare how many bits of information enter on input, how many bits are potentially different on output. Then you would have a measure of complexity of individual functions.
Maybe it's just a general nudging of the language that makes it hard to write bad code?
What if you converted the Scala code back to python? Would it have the same good design? And then, even if it's possible to write beautifully designed code in Python, does it even matter if teams consistently end up writing bad code?
Yeah, this is a hard thing to quantify and a formal proof challenge doesn't really help.
In what sense would such a language be imperative? Are you talking about allowing state mutation? I'm pretty sure that would introduce most of the problems the Python had.
Functional is not so much a thing as the absence of a thing - an imperative language (i.e. a language in which evaluation order is visible and relevant) essentially consists of a functional language plus one or more unmanaged noncommutative effects.
> What if you converted the Scala code back to python? Would it have the same good design? And then, even if it's possible to write beautifully designed code in Python, does it even matter if teams consistently end up writing bad code?
Good coding is refactoring, just as good writing is rewriting. If you converted the Scala back to Python it would have its current beautiful design for now, but as you worked on it the design would decay, because it's so much harder to safely refactor imperative and untyped code, so you do less of it, and it becomes harder to see the essence of the code that should be properly factored, in a vicious cycle.
This. If you only use local (i.e., stack) variables, you should be able to directly transform your code into FP using a state monad. Hence I do not think there is a large difference between the two paradigms here.
Plus: Functional Code is easier to reason about. At least for the person that does the formalization. You simply need fewer constructs (and less complicated ones). The same argument holds for parallel code, btw.
Tail recursive functions and loops are the same thing. Proving a loop correct using invariants and showing (partial) correctness for a tail recursive function by (functional) induction are the same thing.
This is doable in O(n) time and O(1) memory. Sum the list once. Then start from the beginning, collecting a running total and subtracting from the sum for a running difference.
You can also have your legacy cake and eat it too with this excellent recent paper on gradual typing https://arxiv.org/pdf/1802.00061v2.pdf
"This allows for the introduction of new typing features to legacy languages and codebases without the enormous manual effort currently necessary to migrate code from a dynamically typed language to a fully statically typed language. Gradual typing allows exploratory programming and prototyping to be done in a forgiving, dynamically typed style, while later that code can be typed to ease readability and refactoring."
Also, strongly agree on zero overlap between bulldogs and theorem provers. Those who were assholes didn’t make a single effort to contribute productively to the discussion. A good reminder that jerks (no matter how brilliant they think of themselves) can be safely ignored.
I believe the first sentence and here is my personal justification for it (maybe it can be made into rigorous argument). I base this on my experience with Haskell, and it might be that typing and control of side effects is actually essential for the claim.
In Haskell, for the most part, results of a function depend solely on its arguments. So you can treat the inner workings of function as a black box, and only worry about the "boundary" of type information of its parameters.
Now imagine you're facing a large program and you want to estimate an effort required to make a change. In functional programs, if you look at a function, you can see the scope of what the function does from its type (its parameters). In imperative programming, a function can do anything to the system under the hood, there are no natural boundaries.
It's very similar to the real world, where you can estimate for example effort in building something, like renovating an appartment, solely based on the size of the object. You know immediately that renovating a small appartment is (most likely) less effort than building a skyscraper, because of its size. In imperative programming, we're often faced with TARDIS-type deals - bigger on the inside than on the outside.
In physics, there is divergence theorem that formalizes this notion of "you don't have to look inside the object, you can only look at what happens at the boundary". Similarly, functional programming (when done right) creates the boundary at the function level, so you can then apply this type of reasoning to it.
"I chose correctness because it was the easiest to objectively verify. I’m sure that if I posed a similar challenge about refactoring code, everybody would be telling me that “being easier to reason” isn’t about refactoring, it’s clearly about correctness!"
I am not sure he is right there. The setting up of the boundaries in functional programs is real. Yet, with current type systems, the boundaries are not watertight. And of course, you can always write your program in imperative style with functional programming language, without an effective boundary.
I think the OP ignores the boundary setting question, because if you want a full proof of something, then you don't need to have the boundaries. But that's what ultimately helps in understanding. Maybe if he tried to prove several different statements about the code, then the boundaries would help, because he could reuse the theorems about things delineated at the boundary.
I think working with FP correctly essentially forces you to prove statements about the code (for example, this function doesn't have side effects), and then you can reuse these small statements for formally proving something else about it. Whereas in IP, you don't build these statements, you have to build them for the formal proof explicitly. The resulting proofs, written down, will have the same lengths, but in the FP case some work might have already been done.
So what OP is saying is similar to say, well, divergence theorem is really useless, because at the end of the day, you have to correctly account for all your sources and sinks. Which is true in a way, but it is a useful theorem nonetheless.
And you can transform imperative programs into purely functional programs, e.g. by using immutable arrays to represent the heap, etc. (basically, you could write a CPU emulator in Haskell, and let your program call it).
So from a theorem proving point of view, both paradigms are equivalent.