Lots of us are increasingly interested in formal methods coming out of the labs and ivory tower and seeing more casual usage in industry.
But pitching this sort of thing to management is hard, where if they’ve heard of it at all then they associate it with big brain critical path shit at the highest levels of huge orgs like nasa or aws.
Can’t blame people for not seeing the value yet though.. we need to make things easier/cheaper. Plain old testing is often seen as a cost/effort sink that dev teams and management resent and so of course Model checking looks like a whole different layer of ambiguously-worthwhile effort.
Mere advocacy here won’t win people over, because they care more about costs than “correctness” as an abstract virtue. We probably need progress on things like generating code from models and models from code if we want to see more adoption
I agree, and part of the issue is that if the formal methods work as intended, then by design nothing interesting happens, making their success less visible to managers that aren't paying close attention. Ideally something like TLA+ would catch a bug that you wouldn't notice for multiple years (e.g. infinite money glitches), but that means that value becomes less obvious because it can take multiple years to manifest, and that means you're waiting multiple years for TLA+ to show its value, which would be "nothing happened", which can be harder to measure.
I've debated trying to write a PlusCal->Java transpiler [1], and I haven't really ruled that out yet; while I don't think it should be necessary to have that for PlusCal to be useful, I think it would potentially sweeten the sales pitch.
[1] I think PlusCal would translate better to a sequential Java style program than raw TLA+ would.
Why don't you try using PlusCal/TLA+ on some portion of the code at work (if you still care to stay there) to prove its effectiveness? Whittle down the code to something basic to show how it'd work so your manager/co-workers can see for themselves on code that they're reasonably familiar with.
Unless your manager/colleagues are intimately familiar with such tools, I'd think that your touting their usage at work, is more like wishful thinking.
But pitching this sort of thing to management is hard, where if they’ve heard of it at all then they associate it with big brain critical path shit at the highest levels of huge orgs like nasa or aws.
Can’t blame people for not seeing the value yet though.. we need to make things easier/cheaper. Plain old testing is often seen as a cost/effort sink that dev teams and management resent and so of course Model checking looks like a whole different layer of ambiguously-worthwhile effort.
Mere advocacy here won’t win people over, because they care more about costs than “correctness” as an abstract virtue. We probably need progress on things like generating code from models and models from code if we want to see more adoption