> “Logical soundness must come first. This cannot be done without math.”
I’ve long had this (mistaken?) belief that formal methods and mathermatics do not primarily apply to the areas of computing I’m involved with.
I am involved with business systems that are primarily concerned with the recording of activities. Those activities relate to thing/s, and often involve people and places acting in some role (context). In some ways I am modeling interactions between phenomena, together with the concepts through which they are abstracted. Consider for example a payroll system or a airline reservation system.
How can formal methods and mathematics help in this?
These systems are in one sense ideal for formal methods: they're complex interactions between systems, often coordinating over resources and time, with many easily identified constraints that must be maintained.
On the other hand, they're awful for formal methods to the tune of how expensive and valuable it is to actually get a complete description of what the intended behavior of these systems even is.
The bane of application of formal methods in software is that many practical automated systems are only intended to perform against an incomplete, often somewhat inconsistent, and often rapidly changing goal specification. They could be leveraged very fruitfully against these problems, but to do so would invite a long, expensive requirements gathering process between modelers and business owners. There's some anecdotal evidence that this is a valuable process, but the economics don't work out. Even in circumstances where the benefit is obviously there, formal methods front load cost and thus increase delivery risk in many projects.
I think the right way of bringing these techniques to practical software is through expansion "horseback formal methods": lightweight semi-formal tooling and practice which pays out moderate value for moderate investment. These techniques could be run earlier on in a project and demonstrate the value of formal methods while reducing the eventual cost of implementing the heavy hitting tools later on.
A lot of software engineers practice this already, but don't always have the experience to connect back-of-the-envelope domain modeling to mathematical modeling. Or don't find it sufficiently valuable, which is fair. Hopefully, expansion of popularity in these methods will increase the popularity of making smoother transitions from lightweight modeling to more expensive, formal, comprehensive modeling.
Agreed on lightweight formal methods. TLA+ and Alloy have been really eye opening to use, and it's almost at no cost. They're just tools for expressing logic and analyzing models.
Even those are very heavyweight to my mind. I’m thinking things as simple as applying semantics to flow charts and making state tables. Exhaustive enumeration of small spaces forms a neat on-ramp to more powerful methods, if we choose to treat them that way.
Here "horseback" is a term I'm using to mean "applied in the field, cutting corners as needed to make things valuable now". I'm not sure exactly where I picked it up, but I like the idea.
I generally give these business systems the name of "interactive information systems." That's exactly primarily what I work on as well (and I imagine what most people work on, but not all of course).
Maybe counterintuitively, this kind of system is what brought me to math. I kept hearing things like "oh this is just a CRUD app" and it's a solved problem - yet we were opening 50 bug tickets per week (and that's not an exaggeration, we have a large application, and we measure our bug intake and report on it every sprint).
So the first place where math can help with this is at the source - the data! I know not everyone is using a relational database, but the relational model of data is firmly based on math. Learning more about set theory explicitly has improved my interactions with our relational DB immensely.
In my experience, I was taught data access through ORMs. Honestly, the relational model is so much simpler and more elegant. I read somewhere that Edgar Codd used to express relational queries using only predicate logic notation, and I imagine that that would be so much simpler than SQL, and certainly more simpler than bloated ORM code.
On the query front, we like to treat the database as an implementation detail, but I find that this is not practical. Practically, lots of domain logic has to live in queries. I have had 2 bugs recently where a query itself was not returning the right data. Improving my formal reasoning via sets and predicate logic has improved my querying immensely.
I may be wrong, but it seems your design architecture is similar to “structured design”. Where you model data, and alongside that the transformations to be performed on that data. Traditionally this might have been documented using entity-relationship and dataflow diagrams.
In our case, we model our complex business problem domain using an object model independent of persistence and any particular user/system interaction. Perhaps unusually for these days, we also model the many constraints (business rules) within the object model.
Given that the nature of our domain model is not based on transformations that I guess are more easily quantified (or as Dijksta would say “calculated”), I’m still unsure that formal methods would apply or bring any benefits to us at large, other than perhaps some areas of specific behavior?
they can help you avoid malformed requirements. and/or preempt situations such as "oops your reservation has vanished because a bug; but now thanks to your complaint we've fixed it!"
I’ve long had this (mistaken?) belief that formal methods and mathermatics do not primarily apply to the areas of computing I’m involved with.
I am involved with business systems that are primarily concerned with the recording of activities. Those activities relate to thing/s, and often involve people and places acting in some role (context). In some ways I am modeling interactions between phenomena, together with the concepts through which they are abstracted. Consider for example a payroll system or a airline reservation system.
How can formal methods and mathematics help in this?