Though you alluded to it, read-after-write and write-after-write are incredibly difficult at nearly any scale of concurrency. Do you use locking, where even if you have a great acquisition-is-initialization sort of scheme, it gets bad if the locks are held too long? Or do you reconcile after the fact, potentially subjecting users to difference merging? Difference merging already causes angst in programmers, I can't imagine asking normal users to do it.
On the subject of proof languages, I'm extremely pessimistic. I feel like the only thing Prolog proves is that declarative languages can't really exist: writing correct (much less efficient) Prolog code means writing it against the behavior of the evaluation engine. That's not really any different from imperative programming. I never learned Coq, mostly because Prolog left such a bad taste in my mouth. Likewise with Idris, I wanted to like it, but could never find anything that actually made it better than Haskell.
The overall problem with bugs is, apart from hardware exceptions like invalid pointer dereference and integer divide by zero, a "bug" is software doing something other than what you intended. The challenge, then, is coming up with a formal language of intent—which is what programming languages already are. Proofs can only ever be a stripped-down analog of the language you're actually using, but once you try to scale proof specification up, it becomes just as error-prone. Or maybe more error-prone, since proof systems are themselves quite obtuse and complicated.
Do you use locking, where even if you have a great acquisition-is-initialization sort of scheme, it gets bad if the locks are held too long? Or do you reconcile after the fact, potentially subjecting users to difference merging?
"It depends" what you value most:
Do you need 100% correct values?
Or do you need to have values, regardless whether they are correct or close to?
Back to the CAP theorem. There's no correct answer, you need to choose. And the choice depends on your business requirements. Nowadays, the trend is toward Availability but I'm pretty sure that banks will frown upon that and value Consistency instead.
For further actions, you may consider blocking this person and/or reporting abuse
We're a place where coders share, stay up-to-date and grow their careers.
Though you alluded to it, read-after-write and write-after-write are incredibly difficult at nearly any scale of concurrency. Do you use locking, where even if you have a great acquisition-is-initialization sort of scheme, it gets bad if the locks are held too long? Or do you reconcile after the fact, potentially subjecting users to difference merging? Difference merging already causes angst in programmers, I can't imagine asking normal users to do it.
On the subject of proof languages, I'm extremely pessimistic. I feel like the only thing Prolog proves is that declarative languages can't really exist: writing correct (much less efficient) Prolog code means writing it against the behavior of the evaluation engine. That's not really any different from imperative programming. I never learned Coq, mostly because Prolog left such a bad taste in my mouth. Likewise with Idris, I wanted to like it, but could never find anything that actually made it better than Haskell.
The overall problem with bugs is, apart from hardware exceptions like invalid pointer dereference and integer divide by zero, a "bug" is software doing something other than what you intended. The challenge, then, is coming up with a formal language of intent—which is what programming languages already are. Proofs can only ever be a stripped-down analog of the language you're actually using, but once you try to scale proof specification up, it becomes just as error-prone. Or maybe more error-prone, since proof systems are themselves quite obtuse and complicated.
"It depends" what you value most:
Back to the CAP theorem. There's no correct answer, you need to choose. And the choice depends on your business requirements. Nowadays, the trend is toward Availability but I'm pretty sure that banks will frown upon that and value Consistency instead.