Question

Is it wise to pursue math not endorsed by the community? Reflections on Leslie Lamport's Program Model Checking

Answer 1

People have been complaining about the poor adoption of formal verification methods for as long as I can remember. There's an assumption behind all these complaints: the assumption is that there is a substantial unfilled niche for those systems to fill.

However:

* Most people don't care enough about the correctness of their system to even bother writing a specification, let alone formally verifying it.*
* Most systems are simple enough that if you do care about correctness, you can easily prove it without computer assistance.
* Most specification issues can be detected by simple testing, even if formal verification is omitted.
* Most people don't implement their specs correctly anyway.
* Many abstractions are leaky enough that formal verification in the abstract domain does not eliminate the majority of bugs in the real system.

If you are in any of the above cases, formal verification does not give you much benefit. The remaining niche is very small and formal verification techniques *are* widely used there. So I'm not sure how much room there is for more adoption. If you are going to develop these systems, you should probably not measure your success by the percentage of software developers who use them. That is just a recipe for disappointment.

*We can wring our hands as much as we like about how wicked those people are to deprioritize correctness. I don't like it either, but while we are busy wringing our hands, they are busy launching their products and getting all the money. Maybe they are more realistic than we are about the relative risks of a lurking correctness issue in the spec compared to, say, a bug in the implementation, a leaky abstraction, or a user error.

Answer 2

My advice (if one wishes to pursue math not endorsed by the community) is to do JUST ENOUGH math endorsed by the community to gain recognition and a comfortable career, and then spend the rest of one's time on one's passionate pursuits.

With that said, once you gain enough name recognition, you become part of the community and so your endorsement endorses your own research.

Answer 3

Mainly depends on whether your well-being hinges on the goodwill of the community. Here, well-being can mean financial well-being (as in: you need a job) or mental well-being (as in: you require positive feedback for your own mental health).