[rramadass]

Your ideas about Formal Methods are not clear nor quite correct.

Read first the paper On Formal Methods Thinking in Computer Science Education to understand the different levels of practice available. Here is a previous comment of mine which explains and links to the paper - https://news.ycombinator.com/item?id=46298961

Carroll Morgan just published his Formal Methods, Informally: How to Write Programs That Work which teaches you how to think in a formal method manner before you start using the heavyweight tools - https://www.cambridge.org/highereducation/books/formal-metho...

Also read Understanding Formal Methods by Jean-Francois Monin to get an overview of some of the tools and the concepts/mathematics embodied in those tools.

With just the basic ideas from the above viz. Set Theory, Predicate Calculus, learning to think of a Program as a trajectory through a state space, you can start enforcing the trajectory using simple asserts(i.e. predicates) for preconditions/postconditions/invariants. Now because of Curry-Howard Isomorphism (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...) you can treat "propositions/formulae as types" and thus exploit the type system itself as constraints enforcing the above trajectory.

Once the above is grokked, you can move on to more complex logics (eg. FOL/HOL/Temporal/Separation etc.) and learn about tools/methodologies which implement them (eg. Alloy/B-Method/TLA+ etc.).

Finally, with AI tools, the threshold for the practice of formal methods has dramatically come down. This enables one to do Formal Specification and Verification with guaranteed traceability for AI-generated code which IMO is a necessity.

[jdw64]

However, I don't know things as deeply as you do; I only know the basic framework. So you're right that I don't know it deeply. If you have time later, please teach me that part, and I will gladly study it As you said, starting from the light parts and applying them directly might work better for me too. I would appreciate it if you could recommend a few books

[jdw64]

I'm sorry, but what you've said are things I've already read.(this:https://research.tue.nl/en/publications/on-formal-methods-th...)

The points you're raising are not what I'm arguing.

What I am arguing is this:

Formal verification only guarantees consistency between the 'specification' and the 'implementation.' It does not guarantee that the 'specification' correctly reflects reality. This is a problem of modeling.

For your logic to hold, it would imply that humans can formalize, to some degree, the amount of loss that occurs when modeling reality. That is not possible.

It only tells you whether the implementation satisfies the specification. That's also what the OP's post is about. The point that 'the cost has been lowered due to AI' is largely no different from simply saying 'the cost of implementation has gone down.' The real question is whether that implementation properly reflects reality.

The OP's post is fundamentally about 'internal invariants.'

But if you look at the beginning of the first post: 'But outside of some special cases (notably, hardware synthesis), our sense has been that formal methods were just not worth the costs for us. And those costs are really high! seL4 is a great example of this. It's a formally verified microkernel, and a profound achievement. But, boy was it expensive to do! It took 25 person-years of effort to verify 8,700 lines of C, and each line of code required something like 23 lines of proof and a half a person-day to verify.' And the post suggests extending existing methodologies. I think a limited case and generalizing it are different problems. The point is that not every special case is general.

That is why I pointed out whether this extension of methodology is even possible. I am skeptical on this point.

If you want to criticize me, rather than talking about such methodologies, you should criticize the essence of my logic: whether even offensive programming properly understands modeling. I am not simply opposing the OP's post; rather, I am asking whether modeling in the age of AI agents is comparable to modeling in the past.

The materials you shared for me are helpful, but I am saying they do not align with my logic.

Your introduction says: '===== The Problem: Realism vs. Idealism =====' Right?

The question is whether the idealism you advocate actually reflects reality. I am simply arguing for modeling. The gap in my argument is that 'then, because modeling also changes frequently, couldn't all methodologies become useless?' That could be a potential flawed skepticism. But what you're saying is not that.

Every argument has a blind spot. But you are not reading the weak points of my argument; you are only reading your own strong points. This only creates friction and leads us to argue about our emotional differences. I think you are intelligent and knowledgeable. But the points you're raising are not the points of criticism I intended, and what you're pointing out is not what I said.

I am not saying that all methodologies are wrong. I am saying that a methodology can go wrong if it steps outside its boundaries.

However, the fact that you linked me to things I could study was, I think, a gesture of goodwill, assuming that I, as a junior programmer, was misunderstanding something and trying to help me learn. But criticism that assumes I just don't understand isn't helpful for either of us.

[rramadass]

Let me see whether i can explain things better.

> Formal verification only guarantees consistency between the 'specification' and the 'implementation.' It does not guarantee that the 'specification' correctly reflects reality. This is a problem of modeling.

> For your logic to hold, it would imply that humans can formalize, to some degree, the amount of loss that occurs when modeling reality. That is not possible.

Not quite true.

You model reality by mapping your chosen abstractions from the problem domain onto some solution domain. The language of Mathematics was standardized so that we can communicate our problem domain concepts using a "Formal System" (i.e. set of symbols, syntax, rules etc.) to build a "Mathematical Model" (i.e. the interpretation of the above symbols in some real-world domain). The advantage here is that, the mathematical model is precise/well-defined and thus amenable to mechanical manipulation/checking using the rules of symbolic logic by a human/machine.

So the requirements engineering process identifies real-world problem domain concepts/objects/features/usecasees, expresses them using a formal system notation (eg. The Z notation language) to build a unambiguous self-consistent mathematical model. This is the "Formal Specification" for a system. Because it is unambiguous, there can be no confusion in interpretation between all stakeholders. When requirements change (doesn't matter how often), the model is updated but because it is a formal system any inconsistencies can be immediately detected and fixed to bring the system back to a self-consistent state.

The above is basically a realization of the "Scientific Method" viz. Observe, Measure, Hypothesize, Test, iterate (over all of the previous) so that you converge with arbitrary precision towards a desired mapping of your chosen reality.

In this regard see the classic essay The Unreasonable Effectiveness of Mathematics in the Natural Sciences - https://en.wikipedia.org/wiki/The_Unreasonable_Effectiveness...

> The point that 'the cost has been lowered due to AI' is largely no different from simply saying 'the cost of implementation has gone down.'

There is a subtle but important distinction. AI-generated code is probabilistic i.e. for the same exact specification/prompt every run will produce slightly different code. So verification becomes far more important in assuring system robustness i.e. correctness w.r.t. specification. Using AI-agents you can do implementation(i.e. coding) + verification as easily as implementation only. But of course you have to study formal methods and know what to do so that you can instruct an AI-agent do it.

> The OP's post is fundamentally about 'internal invariants.'

No, the OP is merely pointing to a basic conceptual idea which helps one to do formal verification i.e. invariants -> verification conditions -> proof -> theorem.

> But if you look at the beginning of the first post: 'But outside of some special cases (notably, hardware synthesis), our sense has been that formal methods were just not worth the costs for us. And those costs are really high! seL4 is a great example of this. It's a formally verified microkernel, and a profound achievement. But, boy was it expensive to do! It took 25 person-years of effort to verify 8,700 lines of C, and each line of code required something like 23 lines of proof and a half a person-day to verify.' And the post suggests extending existing methodologies. I think a limited case and generalizing it are different problems. The point is that not every special case is general. ... That is why I pointed out whether this extension of methodology is even possible. I am skeptical on this point.

This refers to difficulties using formal methods pre-AI era, because you had to learn special mathematics, methodologies and tools to use this maths all of which are non-trivial. So people only used it for critical problem domains where the labour was worth the cost. But with AI, this constraint is no longer true and so all problem domains are amenable to formal checking provided of course you get the formal specification right.

> I am asking whether modeling in the age of AI agents is comparable to modeling in the past.

Modeling in the age of AI can be done far more faster i.e. far quicker turnarounds to converge your understanding of requirements and verify it simultaneously.

> The question is whether the idealism you advocate actually reflects reality. I am simply arguing for modeling. The gap in my argument is that 'then, because modeling also changes frequently, couldn't all methodologies become useless?' That could be a potential flawed skepticism. But what you're saying is not that.

> Every argument has a blind spot. But you are not reading the weak points of my argument; you are only reading your own strong points. This only creates friction and leads us to argue about our emotional differences. I think you are intelligent and knowledgeable. But the points you're raising are not the points of criticism I intended, and what you're pointing out is not what I said.

I have already addressed these in the beginning of this post.

PS: I am assuming you wrote your above comment after your sibling comment here - https://news.ycombinator.com/item?id=48548589 I have already mentioned a couple of reference books and more can be suggested if needed. In particular, i highly recommend the "Understanding Formal Methods" book which is a fire-hose of information. It tries to provide an overview of the whole domain with chapters alternating between mathematical theory and methodologies/tools using the theory. Supplement it with wikipedia/google as needed. After this you can pick up a book/documentation on any specific tool you like eg. Dafny, Lean4, TLA+ etc. with the assurance that you understand the basic concepts and can use the tool effectively.

[jdw64]

Thank you for your comment. I may have been a bit rude, but that was not my intention. I trust you will understand.

Anyway, there are points in your thinking that I also resonate with. I realize now that some of my arguments were too rough.

I am not going to withdraw the point that formal specifications cannot always be specified with perfect accuracy, but I do think there were some shallow aspects to what I said. I appreciate that a programmer like you took the time to write such a thoughtful reply to me. I have also been reading the books you recommended as PDFs. I have learned a lot about areas and methodologies I was not familiar with. Thank you for that.

For now, I am planning to learn more about formal verification as you mentioned. Up to now, I have only been applying very basic methodologies. I mainly used techniques like Result types, algebraic data type modeling, and guard clause based Design by Contract.

The reason I am doing this is that my work mostly involves repetitive tasks, and I think the methodologies you mentioned would fit me quite well. I hope you are not offended.

Thank you for taking the time to engage with my comments, and I also appreciate you taking the trouble to recommend books. I will study them and try to apply what I learn in my work. Have a good day. I feel a bit sorry for having spoken impolitely to you, a senior programmer, as a junior

[rramadass]

That's all right; no need to feel bad. These things happen when communicating in forums like this.

Btw - Another useful way to think about model building (of reality) is analogous to the study of "Accuracy and Precision" usually taught in introductory numerical methods course. Wikipedia has a very nice explanation - https://en.wikipedia.org/wiki/Accuracy_and_precision Formal Methods help with precision and consistency. But of course you could be modeling the wrong requirements and thus it would not be accurate. Accuracy requires human intelligence (i.e. domain knowledge) but AI can help here too. You can structure the domain requirements (formally or not) and engage in socratic dialogue with an AI-agent to refine your understanding of the problem and converge towards the "truth" i.e. a set of requirements acceptable to all stakeholders. There are actually a bunch of startups working on this eg. Entalpa - https://entalpa.com/en

Some additional resources to help one better understand the concepts behind formal methods;

Faultless systems: Yes we can! - https://www.research-collection.ethz.ch/entities/publication...

The Faultless Way of Programming - https://dl.acm.org/doi/fullHtml/10.1145/3698322.3698340

The Digital Maieutic: Socrates and the Art of Prompting - https://news.ycombinator.com/item?id=48342887

Finally, see Industrial-Strength Formal Methods in Practice for case studies and practical advice - https://link.springer.com/book/10.1007/978-1-4471-0523-7

[jdw64]

Thanks! I will make sure to read the last book thoroughly. Have a good day