Something I've wondered about for a while, but I usually think is a bit too crazy to mention in public, is that one way to formalize Dirac deltas might be somewhat like algebraic effects. A Dirac delta is an algebraic effect whose handler finds the limit of the surrounding expression as you apply it to a sequence of Gaussians (say) whose width goes to zero. The reason I like this is that it corresponds very well to how a physicist might talk about a Dirac delta: "you have to understand what we mean is that if you see an expression with a delta in it you take a limit like so..."
Sure, there's already machinery in functional analysis for working with Dirac deltas. But algebraic effects may actually fit better with how I think. I think Bartosz Milewski (npub1glg…tqzy) has talked about the similarity between distributions/generalized functions with the handling of continuations, so a formalization via algebraic effects would probably work out quite well.