"I love me a powerful type system, but it’s not the same as actually running your software in thousands and thousands of crazy situations you’d never dreamed of."
Would not trust. Formal software verification is badly needed. Running thousands of tests means almost nothing in software world. Don't fool beginners with your test hero stories.
That'll work great for your Distributed QSort Incorporated startup, where the only product is a sorting algorithm.
Formal software verification is very useful. But what can be usefully formalized is rather limited, and what can be formalized correctly in practice is even more limited. That means you need to restrict your scope to something sane and useful. As a result, in the real world running thousands of tests is practically useful. (Well, it depends on what those tests are; it's easy to write 1000s of tests that either test the same thing, or only test the things that will pass and not the things that would fail.) They are especially useful if running in a mode where the unexpected happens often, as it sounds like this system can do. (It's reminiscent of rr's chaos mode -- https://rr-project.org/ linking to https://robert.ocallahan.org/2016/02/introducing-rr-chaos-mo... )
Formal verification require a formal statement of what the software is supposed to do.
But if you have that, you have a recipe for doing property based testing: generate inputs that satisfy the conditions specified in this formal description, then verify that the behavior satisfies the specification also.
And then run for millions and millions of inputs.
Is it really going to be worth proving the program correct, when you could just run an endless series of tests? Especially if the verifier takes forever solving NP hard theorem proving problems at every check in. Use that compute time to just run the tests.
Great, but formal software verification is not yet broadly applicable to most day-to-day app development.
Good type systems (a pretty decent chunk of formal software dev) are absolutely necessary and available.
But things get tricky moving past that.
I've tried out TLA+/PlusCal, and one or more things usually happen:
1) The state space blows up and there's simply too much to simulate, so you can't run your proof.
2) With regard to race-detection, you yourself have to choose which sections of code are atomic, and which can be interleaved. Huge effort, source of errors, and fills the TLA file with noise.
3) Anything you want to run/simulate needs an implementation in TLA+. By necessity it's a cut-down version, or 'model'. But even when I'm happy to pretend all-of-Kafka is just a single linkedlist, there's still so much (bug-inviting) coding to model your critical logic in terms of your linked list.
Ironically, TLA+ is not itself typed (deliberately!). In a toy traffic light example, I once proved that cars and pedestrians wouldn't be given "greenLight" at the same time. Instead, the cars had "greenLight" and the pedestrians had "green"!
Would not trust. Formal software verification is badly needed. Running thousands of tests means almost nothing in software world. Don't fool beginners with your test hero stories.