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"!
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"!