See the other thread (oops, it got flagged). Mainly, the right level of abstraction is that of a logic. Current logics are somewhat lacking (first-order logic doesn't have general binding, typed logics don't have a single mathematical universe), but I think I found the one to rule them all. Programming is then just a (arguably very important) special case of expressing yourself in this logic. Hopefully soon(ish) on a website near to you.
