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

3 Answers

0 like 0 dislike
0 like 0 dislike
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.
0 like 0 dislike
0 like 0 dislike
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.
0 like 0 dislike
0 like 0 dislike
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).

Related questions

0 like 0 dislike
0 like 0 dislike
2 answers
a_dalgleish asked Jun 21
Contributing to the right math area, If all areas are equally curious
a_dalgleish asked Jun 21
0 like 0 dislike
0 like 0 dislike
3 answers
bendiek asked Jun 21
Math on GitHub: The Good, the Bad and the Ugly
bendiek asked Jun 21
by bendiek
0 like 0 dislike
0 like 0 dislike
16 answers
AdamGreen asked Jun 21
Books used in undergrad math at colleges outside the United States.
AdamGreen asked Jun 21
0 like 0 dislike
0 like 0 dislike
7 answers
DisruptorMgmt asked Jun 21
Oeisle , guess the math sequence from OEIS.
DisruptorMgmt asked Jun 21
0 like 0 dislike
0 like 0 dislike
67 answers
chandanjnu asked Jun 21
How do I get rid of the destructive mindset that Applied and Statistics are "lesser" than Pure Math
chandanjnu asked Jun 21

24.8k questions

103k answers

0 comments

33.7k users

OhhAskMe is a math solving hub where high school and university students ask and answer loads of math questions, discuss the latest in math, and share their knowledge. It’s 100% free!