I've been running infxludb 0.9 + heka 0.9.x + grafana 2.x stack in a production environment for over a month. Mostly successful, although I find the grafana tooling for building queries to be a bit weak. I think there are improvements coming soon to address this, though.
Overall, influx performance seems to be pretty good although we aren't ingesting enough data to say anything really concrete. We also make use of continuous queries to aggregate our time series, which of course makes large-interval queries more efficient.
As Kyle himself mentioned (I think it might even be in relation to this document), Jepsen cannot prove that your software is safe, only prove that it isn't.
He even called them out for modifying timeout value to pass the tests[1].
> Jepsen cannot prove that your software is safe, only prove that it isn't.
This doesn't just apply to Jepsen but to all software tests. You only ever test a finite set of scenarios, so you can't really ever guarantee your software is 'safe'/bug-free - only that it does not fail in common/expected scenarios.
Depending on how large "software tests" is in your mind this can easily be not the case.
Kyle often mentions the tool TLA+ which enables complete and total formal analysis of certain systems. This can be a test which is complete and therefore a positive proof of correctness.
It's also not difficult to test smaller components of your system if you note that the state space here is small enough to be exhausted. This is a very important thing to look in to in serious, important components of a software system.
Finally, though it's futuretech today still, dependent types offer a general system for embedding proofs of correctness directly into code thus elevating positive proof to a computational artifact just like any other.
Type systems and proofs have their limitations, if just because for a proof to be worth anything, I need a perfect description of what I want, and that doesn't make any sense outside of trivial cases.
I once worked with a relatively well known, prove everything developer that you might know by name. He's written books and everything. He built an algorithm to make a distributed system of equal peers figure out when it needed to start more nodes, or could shut some of them down. He wrote a proof, in code. He wrote a paper. When in production, the system would not work as advertised, and he blamed it on other pieces, because the algorithm was proven correct! So the problem stayed there for months.
After he left the company, I decided to figure the problem out, so I read through the proofs, the paper, and the code: All the single letter variables you could possibly want. I figured out that yes, the algorithm was flawless, as long as every operation in the system was atomic and instantaneous. Instead of the proof, I built a small simulator that didn't have such flawed assumptions, and got the exact same behavior as the production system. So the proof was perfect, as long as we made assumptions that are impossible in our universe. And the entire algorithm was less than 200 lines of code.
So whenever we have a reality that is difficult to model (and let me tell you, distributed systems fit the bill), dependent types will not save you, haskell or no haskell. Proofs will always be limited by your assumptions.
So while the tools you mention are nice. They hit the same limits as everything else we build. Whether to write a proof in idris, use generative testing, or just some example testing, is really all a tradeoff, but you will never escape from bad specification, as all specifications are bad.
But that said, the style of analysis is totally different in each case. It's not true that you can never prove correctness. It's just a certain option with certain tradeoffs.
And there are success stories! Tons of older ones back when proof was a major component of compute programming. More modern ones like validated C kernels and compilers.
I don't know of any case in industry where TLA+ has been used to prove a spec correct. AFAIK it's only been used for model checking. Read the "Formal Methods at AWS" paper for details.
FWIW, I've found running supervisord for all containerized apps with a log redirect to a host-mounted path to be a perfectly reasonable solution.
I would hate to see docker go down a path where it folds in its own logging "framework", which, I feel, would be going too far (poor separation of concerns, etc).
Well from a 12-factor app perspective, having each container dump its output to stderr/stdout is basically perfect as long as docker has a pluggable mechanism for dealing with that output. The "docker attach" API is all that you need, since you can attach prior to starting the container. Then you just need a way to tell docker not to save the logs via some "--disable-logging" option to "docker run" and "docker start".
I fully agree that TDD has turned into a cargo cult obsession for many developer shops. The benefits of unit tests are usually for the developer, but in over abundance can lead to inflexibility and debt when your system needs to change.
Part of the problem is developers are often too hesitant to delete tests. Tests, like any code, should be deleted when their value is lower than their cost. Tests have maintenance cost like any other code. Plus they add to the time it takes to produce a build.
When making significant changes to implementation of something it's often worth just leaving acceptance tests in place for regression and deleting unit tests and TDDing your new implementation
TDD has turned into a way for devs to 1-up other devs. When testing becomes a discipline of its own with the knowledge of these testing frameworks, something has gone wrong. Tests shouldn't need much more than assert statements, and maybe a little extra.
> in over abundance can lead to inflexibility and debt when your system needs to change.
I hear this argument a lot, and I think it is absolutely incorrect. If tests are hindering your system then you're just doing it wrong. It's like saying "climbing rope is a hindrance for the rock climber, since I have tied gordian knots around my feet and now cannot move."
TLDR doing something badly doesn't mean the thing you have botched is itself bad.
Yes, this is really what I mean by "over abundance". I'm suggesting that excessive application of unit test "fundamentalism" can lead to a variety of problems. A particular manifestation of what you describe as "doing something badly".
