4 ms·
I'm experimenting with including formal methods on my team. We're working with concurrency in an event-sourced system and want to be reasonably certain our desi
by agentultra 8y ago
I'm experimenting with including formal methods on my team. We're working with concurrency in an event-sourced system and want to be reasonably certain our design is correct. We're also working on deeply embedding our specifications into our test suites to address some of the trade-offs mentioned near the end. We like to eat our cake.
I'm down with advocating more use of formal methods in industry and open source. The cost of using these tools has come down at such a rapid pace in the last decade or so compared to the rising cost of complexity our system designs are taking on. It's starting to make the trade-off attractive imho.
- gbacon 8y agoI’m also supporting a customer who is using a stratified approach to verification and validation on mission-critical code stratified into layers of static analysis, unit tests, property-based tests, and formal methods.
- jdp23 8y agoAgreed - with better and lower-cost tooling the tradeoffs get steadily more appealing. Back in 2005ish I put together a panel with Kent Beck of extreme programming fame and Martyn Thomas of Praxis, which was doing commercial development using formal methods and Spark/Ada. We were hoping for fireworks but it turns out they were in agreement on a lot of stuff: formal methods need to be used in the context of a pragmatic development process, sometimes iteratively exploring is the right approach, for high reliability you need to complement testing with other techniques like formal methods. Concurrency was one of the examples where there was general agreement that testing and code inspection just isn't enough.
- nradov 8y agoStatic analysis tools for common languages are getting fairly good at detecting many types of concurrency defects.