Modern notational alternatives for the indefinite integral?

I like the Leibniz notation, and I think the reason it's survived for over 300 years and continued to be almost the only game in town is that in many respects it's a miracle of design. Nevertheless it's an artifact of an earlier era in the history of mathematics, and anecdotally I seem to encounter a lot of mathematicians who feel that it's ugly, bad, and illogical. There seem to be two fundamental issues involved: (1) it's commonly interpreted using infinitesimals, which didn't get rehabilitated by non-standard analysis (NSA) until ca. 1960; (2) it predates the notion of a function.

Issue #1 seems to me to be a non-issue. In fact Blaszczyk et al. (see p. 10) have argued that Leibniz and Fermat had a pretty fully developed notation and terminology for what NSA refers to as the "standard part:" they called it "adequality" and used the symbol ${}_{\ulcorner\!\urcorner}$. From this perspective what NSA contributed was nothing more than some systematization of long-established practices and some model-theoretic work that showed that this systematization was sufficient logical justification for those practices.

But I think the complaints about the Leibniz notation may have more merit when it comes to issue #2. For example, in comments in this mathoverflow question, Andrej Bauer complains that:

it's legal to write $\int x^2\: dx=x^3/3+C$ (which exposes the bound variable $x$)

I suggested in that comment thread that this could be OK if one simply interpreted the notation $x$ as the identity function, but Andrej Bauer pointed out that that may not be enough to explain all possible uses of this feature of the notation.

Are there well thought out modern alternatives to the Leibniz notation that would address issue #2? The closest I can think of is something like this:

$ \int x \mapsto x^2 = \{f|\exists C\ f(x)=(x \mapsto x^3/3+C)\}$

This uses the notation $\mapsto$ for constructing anonymous functions, e.g., $x \mapsto x^2$ means the function $f$ such that $f(x)=x^2$. Well, it works here, but it's awfully painful to write. Are there better alternatives that are either used by a significant number of people or that have been "test-driven" enough to show that they're really practical?

This is the notation that I created for my own use. It's based on an alternative to the typical notation for creating functions from 'legacy' expressions using lambda binding. The expression is enclosed in brackets, and the variable to be bound is placed below the right-hand bracket (which isn't ideal, but it's the best I could come up with). I'll try my best to get MathJax to render everything properly: $$f = \Big[x^3 + 5x^2 + 1\substack{\Big]\\x}$$ The bracketed expression can take the usual higher-order functions such as differentiation, inversion, and evaluation: $$f' = \Big[x^3 + 5x^2 + 1\substack{\Big]'\\x}$$ $$f^{-1} = \Big[x^3 + 5x^2 + 1\substack{\Big]^{-1}\\x}$$ $$f(t) = \Big[x^3 + 5x^2 + 1\substack{\Big]\\x}(t)$$ (A sidenote, I also use $f\langle x \rangle$ over $f(x)$ for evaluation to separate it from multiplication, but I'll continue with the standard notation since this question isn't about that.)

For indefinite integration, I take the Lagrange prime notation a step further, and the apostrophe goes on the left side: $$\int f(x) dx = {'f}(x)$$

When combining this with more operations, you can use parentheses: $$('f)' = f$$ $$('f)'(x) = f(x)$$ $$('f)^{-1}$$

Indefinite integrals

When combined with the bracket notation, we get the alternative notation I use for indefinite integrals: $$\int x^3 + 5x^2 + 1\: dx = {^{^{'}}}\Big[x^3 + 5x^2 + 1\substack{\Big]\\x}(x)$$ Some Notes:

-I omit specifying the binding variable when there's only one variable in the expression or it's clear from context which variable is being bound

-I also often omit the evaluation part of the expression (necessary for binding across the equality sign to a 'legacy' expression) when working with derivatives or indefinite integrals, writing things like this: $${^{^{'}}}\Big[x^3 + 5x^2 + 1\Big] = x^4/4 + 5/3x^3 + x$$ which is strictly illegal and is akin to writing $$f = x^4/4 + 5/3x^3 + x$$ This is an abuse of notation I do for convenience, especially during long calculations for indefinite integrals. However, a trivial adjustment could be made to rectify this, by putting some sort of mark or diacritic to indicate that the expression is evaluated using a variable with the same letter as the binding variable. The first thing that comes to mind is a small line crossing through the right-hand bracket, however I don't know how to get MathJax to do this to show what I mean. You could also write $${^{^{'}}}\Big[x^3 + 5x^2 + 1\Big] = \Big[x^4/4 + 5/3x^3 + x\Big]$$ which would be legal.

-The equivalent to u-substitution does not use any other variables (you could sort of use other variables, but it stretches the notation beyond what it's good for, see below). Instead you use the identity: $${^{^{'}}}\Big[f(x)\Big] = {^{^{'}}}\Big[f(g(x))g'(x)\Big](g^{-1}(x))$$ Though in a way you might end up 'using other variables' by defining g so you don't have to explicity write its inverse.

-Indefinite integration using this notation could also be done by treating $\int$ as an operator just like a left-hand apostrophe: $$\int f = \int\Big[x^3 + 5x^2 + 1\Big] = {^{^{'}}}\Big[x^3 + 5x^2 + 1\Big]$$ However this is clearly cumbersome to write, so what I've come up with is a modified integral sign that's bracket-y instead of curly, and takes the place of the left-hand bracket. This serves as a shorthand way of writing it. I again don't know how to make it in MathJax to demonstrate. Essentially you take the bottom tail of the bracket and flip it to face to the left, so it's shaped like an integral sign, but straight instead of curly.

Also, treating $\int$ as an operator can be very useful in this case: $$\int_a^b f$$ rather than $$\int_a^b f(x) \: dx$$

Definite integrals

The modified integral symbol becomes necessary when we want to write definite integrals using this notation. This symbol works just like the standard integral symbol. When limits are placed in it, the result of the bracket expression no longer returns a function, because it is evaluated when limits are placed on it.

When evaluating the limits using the antiderivative, I use something very similar to the standard bar notation: $$\int_a^b\Big[x^3 + 5x^2 + 1\Big] = \Big[x^4/4 + 5/3x^3 + x\Big]_a^b$$ More generally, the placement of two numbers to the right side of a function can be considered a higher-order function: $$\Big(f\Big)_a^b = f(a) - f(b)$$ Before I made the modified integral symbol for using limits with this notation, I considered using a more modular approach by chaining this "difference-evaluator" operator with the antiderivative apostrophe operator. I didn't pursue this much further because I mistakenly believed parentheses would be necessary to disambiguate which operator is applied first, similar to $('f)^{-1}$. However, on writing this I realize that there's only one order which is legal and makes sense. The antiderivative operator must come first because the difference-evaluator does not return a function. Of course, the other option of changing the difference-evaluator to work on the left side of the function would not work well with the apostrophe antiderivative operator, which would end up right next to the top limit.

Other Remarks

-You can put other things besides simple variables as the binders: $$\Big[x^3 + 5x^2 + 1\substack{\Big]\\x^2} = \Big[x^{3/2} + 5x + 1\substack{\Big]\\x}$$ More generally $$\Big[f(x)\substack{\Big]\\g(x)} = \Big[f(g^{-1}(g(x)))\substack{\Big]\\g(x)} = \Big[f(g^{-1}(x))\substack{\Big]\\x}$$ Or, something very experimental $$y = x^2$$ $$\Big[x^4+6x^2+3\substack{\Big]\\y} = \Big[x^2+6x+3\substack{\Big]\\x}$$ $$\Big[x^4+6x^2+3\substack{\Big]\\y^2} = \Big[x+6\sqrt{x}+3\substack{\Big]\\x}$$ Though it's cumbersome to use this for anything useful, and I'm not confident in the correctness of it all, and it can be confusing. Functional notation doesn't mix very well with expression-oriented notation.

-And more on that point, this notation is still not very good with parametric equations or similar types of expression maps where it becomes difficult to frame things in terms of functions. This sort of thing is hinted at in Formalizing Those Readings of Leibniz Notation that Don't Appeal to Infinitesimals/Differentials when they write 'I saw a passage recently that spoke in terms like "x(u) is the inverse function of u(x)"--how should this be understood more precisely?'. I'd appreciate any resources on this kind of thing. This is something I've been intending on thinking about. When it comes to parametric equations, unless there's some better way of framing it in terms of functions, lagrange notation fails and leibniz notation shines (EDIT: I've since realized that it fails spectacularly for second and higher derivatives, see this paper). For instance, if you have $$x=f(t)$$ $$y=g(t)$$ Leibniz notation makes it trivial to conceptualize and find dy/dx without needing to appeal to explicit expressions of the inverses of f and g. Bracket notation can get the job done here, but it's somewhat clumbsy (especially with mathjax!) and needs an appeal to inverse functions (which might be multi-valued): $$dy/dx = \Big[g(t)\substack{\Big]\\f(t)}{^{^{'}}}(f(t))$$ $$ = \Big[g(f^{-1}(t))\substack{\Big]\\t}{^{^{'}}}(f(t))$$ $$ = \Big[\frac{g'(f^{-1}(t))}{f'(f^{-1}(t))}\substack{\Big]\\t}(f(t))$$ $$ = \frac{g'(t)}{f'(t)}$$

-Multivariate binding can be done by using, for example, $x,y$ at the lower right instead of a single variable.

-I highly recommend this paper which ditches expression-oriented notation completely, and uses the identity function instead of 'variables' like x. It has similar advantages to bracket-notation, but is similarly inadequate when it comes to multivariate functions in my opinion. Also, a more distinct symbol for the identity function is needed, because iota looks too similar to 1 or l. Overall I think it's superior to bracket notation.