To me this entire argument "woe us if we run out of work to do" is directly self-contradictory. If people are miserable because they don't have the necessities of life, then, by definition, there's work left to do. On the other hand if there really is no work left to do, then everybody should be perfectly content with their material wealth.
Well, I've spent a lot of time with theorem provers as well as with normal mathematics. I've never experienced an exponential blowup when formalizing mathematical ideas. It would always boild down to step-by-step verification. And I don't see any reason to suspect that the paper under discussion uses non-standard techniques.
You could theoretically put all kinds of meta-information into the grammar, even arbitrary code snippets that are pasted into the generated parser. I'm not saying that that's a good idea - it undermines much of the value of a parser generator - but generally speaking it can be done.
I don't see how a better understanding of the generated parser helps improving those things. Either you can't improve these, or you improve these by modifying the grammar.
Finding flaws in proofs is as easy as verifying them. After all, finding a flaw amounts to just checking a proof. Finding a proof is the truly hard challenge.
I think infinities also have use in the real world. Take the insolubility of the quintic. You can reword this as saying that none of the infinitely many candidate solutions for quintics work. Its real world utility is straightforward: there's no point to continue looking for a solution.
I program in Clojure more than in any other language. That doesn't change the fact that I feel a stronger incentive to avoid local variables than in any other language I've used so far. Also if I wanted to tackle this issue with a macro I'd probably have to make an alternative to `defn`. That's a great way to invent a dialect of Clojure nobody else will be familiar with.
I don't think it's as easy as that. In fact there's probably no single reason accountable for Lisp's lack of popularity. Here's my own personal pet peeve: Declaring local variables creates a level of nesting. Local variables are a great tool for improving code clarity. Having to wrap your logic with `(let [value (...)] ...)` in order make a new local variable is unnecessarily painful.
I'd appreciate a more general appreciation of how little can be accurately predicted. Any time I hear sports commentators predict winners I internally shake my head. Why do so few people have the ability to admit to themselves that most things are just unpredictable?
Douglas R. Hofstadter has written multiple books on the subject. He most directly addresses it in "Surfaces and Essences" co-written by Emmanuel Sander.
It is enjoyable reading and very thorough. Pending revolutionary new insights I might even regard it as conclusive.
Completing the first half of a symbol that I've been typing already works reasonably well with Cursive. What I'm looking for is something that looks at the result of an expression and figures out what other functions can accept that as input. Matching up specced postconditions with preconditions might work, but I'm not sure how well.
I think the spec library that they're putting together right now might be able to solve the error messages. What I'm waiting for is to be able to hit something like dot in my ide and see a list of suggestions, I'm not sure if spec can be leveraged to that extent.