alt Hacker NewsUnfortunately proving anything about a concrete imperative implementation is orders of magnitude more complex than working with an abstraction, because you have to deal with pesky 'reality' and truly take care of every possible edge-case, so it only makes sense for the most critical applications. And sometimes there just isn't a framework to do even that, depending on your use case, and you'd have to sit down a PhD student for a while to build it. And even then you're still working with an abstraction of some kind, since you have to assume some kind of CPU architecture etc.
It really is more difficult to work with 'concrete implementations' to a degree that's fairly unintuitive if you haven't seen it first-hand.
I can't fathom how crazy it gets to model once you try to consider compilers, architectures, timings, temperatures, bit-flips & ECCs, cache misses, pseudo and "truly" random devices, threads, other processes, system load, I/O errors, networking.
To me it seems mandatory to work with some abstraction underneath that allows factoring a lot of different cases into a smaller set of possibilities that needs to be analysed.
It's also how we manage to think in a world where tiny little details do give you a likely insignificantly different world-state to think about.