> As far as FP is concerned, I think that the memory and performance penalties are often too heavy: there's certainly a place for mathematically provable progra

> As far as FP is concerned, I think that the memory and performance penalties are often too heavy: there's certainly a place for mathematically provable programming - I just don't know what it is. FP isn't necessary for mathematically provable programing. Dijkstra and Scholten did a ton of work in this area that conclusively demonstrated that. I can't do them justice in a post here, but to a first approximation the trick is that you reason about imperative programs as transformations on a state space, which is to say you think about functions. A simple example: We want the predicate x = 3 to hold for all preconditions. The code "x := 3" establishes that predicate everywhere in the state space. That is to say, no matter what x was before the assignment, afterwards the predicate holds. While plenty of bytes have been spent on discussing why this is totally impracticable for real programs, whatever that means, we also have buzzwords like "defensive programming" that follow the same philosophy: we should write code such that when it has executed no matter what the state of the system was initially, afterwards it satisfies some specification.