> maybe some combination of static analysis and testing can make sure my implementation matches it?

I'm becoming a fan of the ideas espoused in eg http://www.vpri.org/pdf/m2009001_prog_as.pdf and http://shaffner.us/cs/papers/tarpit.pdf‎ where rather than trying to verify that arbitrary code matches your specification, you make the specification itself executable and then supply hints and heuristics on the most efficient way to execute it. It's a similar idea to first writing an sql query and then hinting which execution plan should be used. Compared to writing arbitrary code this approach limits expressiveness but it removes the verification problem entirely. So far we've only seen this approach used heavily in querying and in constraint solving. Luckily, it turns out that large chunks of the programs we write day to day can be expressed in terms of either database-style queries or constrained search (see eg http://boom.cs.berkeley.edu/).

I think that in the medium term, this is a good place to go. Specify denotation, and operational constraints, and then fill in details whenever the compiler can't figure out the rest.

Actually, the above is how I've been thinking about it for a while, but I'm not sure there's any reason we can't say "denotational constraints" as well - where exact denotation is just a particularly tight constraint.

Okay, how does

   \integral{\integral nasty expresion dx}dy}

get implemented? (excuse the faux LaTex, I never remember the syntax)

Something like that (typing from memory):

  (defun do-integrate (tree var)
      ;; -- do some crazy symbolic manipulation on the source tree
  )

  (defmacro integral (expr var)
     ,(do-integrate expr ,var))

I don't think I expressed my concern very well. The point is is that you often cannot just depend on some built in to do your mathematics for you - stability, speed, and convergence depend heavily on the implementation that you use. There is a huge gulf between symbolic expressions and how we solve them on a computer. For example, all we really know how to solve is Ax=b - linear equations. Oh, we have special tricks for some nonlinear cases, but a huge part of computer math is getting your system approximated as Ax=b, and then solving for that. You can't just hand wave that away by throwing symbols in your code.

People will bring up various symbolic and other specialized math packages. Sure enough, they exist. And, they are dog slow. They are used to explore problem spaces, and to get the solutions to small problems. But when it comes to it, we reach for C++, for Fortran (and now, maybe Julia) to get performant code. If I want to type equations and get results, why wouldn't I already be using one of those systems, heavily optimized for math computations of that sort? If I am in a general purpose language, it is because I need to specify the system in great detail, and obscuring it with symbols like sum and integrate just doesn't work.

And, in case the larger point is lost, this is an example to illustrate the larger case - that we can't really obscure large parts of the computational model. In cases where we can, we already do so. For example, I don't write my own red-black trees, I count on STL to do it for me. v.insert (make_pair("name", "Roger")) is a great abstraction (albeit verbose). But even when it comes to using something like BLAS & LAPACK, I have to choose the representation and so much more. Dense vs sparse, etc. So please don't retort with some integral or other math equation that can be solved efficiently with default methods - that misses the point. CS since the 50s has been a study of how to abstract concepts away, and have a done a fine job of it. A few pictures doesn't magically make the remaining problems disappear.

edit:

I somewhat know what I am talking about here. In my Ph.D program (left it, didn't graduate, not claiming a PhD) in the 80s my advisor was advocating an expert AI system to resolve these problems. Any guess as to the result of that research? The hint is that no expert system is built into any of our heavy math systems today. And just this week I sat through a session where a researcher was presenting early work he was doing no a DARPA grant to, wait for it, same thing, basically.

It's a outrageous, tremendously hard problem, and we keep getting people announcing that they have solved it, they just don't quite have the code running yet. Okay. Show me, don't tell me. A point-click interface to inject a sqrt symbol into my code, or an image of a playing card, is so far from the mark, both from the triviality of it, and the distance between that and a hard problem.

My points where 1) that these kinds of concerns are entirely orthogonal to whether we limit our expression to ASCII symbols, and separately 2) that there can be useful things done with analytic forms even when we aren't able to turn them directly into machine code.

It's like you didn't read what I said.