In other words, because GEN AI a lot of code, the idea is to shift human value toward verification. Sometimes I think about what programming really is. In fact, learning programming itself is a huge challenge for a non English speaker like me. I have to rely on machine translation to understand English documents that have no translation. The materials in my language are about 5 to 6 years behind.
Now, since it's impossible to code review the tens of thousands of lines of code that AI produces, I see discussions about establishing an absolute rule like mathematical proofs. Reading this reminds me of Rust's borrow checker. In fact, after writing in Rust a few times, it often leads to bad practices where people use tricks to avoid the borrow checker.
Actually, when mathematical rigor goes too far, humans tend to find ways around it. An undereducated programmer like me is especially prone to that.
Looking back at this kind of attempt, it will probably result in writing code only for specific formalized answers. If it becomes that standardized, I'm not sure it will be able to respond to human needs.
I think these defensive programming attempts are fine, but I want to do offensive programming (I coined that term). You take risks, but you fix things quickly and ship. Believing that over time, it will become good enough. Of course, for established industries where accuracy matters and the scope of work is well defined, like Jane Street, the approach in this article is correct. In other words, because there is enough data to adequately model the market's demands
But for social losers like me trying to make money, constantly moving from place to place looking for gold mines, these kinds of methodologies seem like a luxury.Established businesses with mature modeling need highly educated and specialized personnel to continuously optimize. But I know that realistically, I can't keep up with that demand. So I look for places where modeling is unstructured, but I'm not sure if I can use this approach even then.
> I want to do offensive programming (I coined that term). You take risks, but you fix things quickly and ship.
Nice, I like the term too. But the paradigm is absolutely status quo in the industry. The thing is: with Gen AI the cost of "defensive programming" has gone way down, while the cost of (human) verification has gone way up. On the other hand, formal methods make verification cheap but come with massive implementation overhead (writing specs, types, proofs, and generally bending the implementation into a rigid framework). But Gen AI can automate all that laborious work. It's a match made in heaven.
You're right. I think the point we need to discuss here is, to be clear, dividing the contexts in which defensive programming is strong and where it should be aggressive.
I think the overhead of implementation is enormous, but I believe AI can write it. However, before even reaching the 'implementation' stage, that is, at the planning stage, sufficient data must be collected for the implementation to be safe.
In that respect, I think Jane Street already has enough data and modeling capabilities. However, I think it's a bit difficult to say whether this approach will take shape in many other domains.
In that sense, I also think that the reason many industries are doing this kind of fast deployment and experimental tooling might be a preparatory step for that kind of modeling. Have a good day Thanks for the good comment. It helped me think more sharply as well
> I think the overhead of implementation is enormous, but I believe AI can write it. However, before even reaching the 'implementation' stage, that is, at the planning stage, sufficient data must be collected for the implementation to be safe.
I don't really follow here, I think once you know what you want the system to do, you could start to model it formally. What data do you think needs collection for planning here? Is it just for performance profiling of whatever algorithms are decided on? But that seems equally as relevant as if you do your initial implementation straight-up in code w/o any formal approach.
Formal verification is a mathematical proof and requires axioms. However, if real world field data is not collected, you are not comparing theory to reality but forcing reality to fit the theory, like the bed of Procrustes.
This means the object of verification is not reality but the consistency between specification and implementation, and incorrect formal verification only refines a wrong worldview.
A company with sufficient capital can turn a theory into reality through marketing and other means. But for small businesses or in markets where new competitive logic is introduced due to the lifespan of an industry, this can be a fatal problem.
For example, consider the stock market. If you use the Buffett indicator to invest right now, the market looks overheated. But other indicators suggest positive prospects. We cannot know whether the market logic of the AI era aligns with the past or is different, but I believe there are cases where modeling changes due to real world shifts.
In reality, when converting the real world into mathematics or physics, information loss is inevitable. In this process, science may later advance and become more precise, or a value once considered important may turn out to be wrong.
In other words, something may be correct within a given set of axioms, but those axioms themselves may change depending on the context. The history of computer standards has shown this as well(ASCII -> Unicode)[To explain this point, ASCII works perfectly in English speaking countries, but in my country it creates incorrect encoding.]
Programmer's ability may come down to distinguishing between what changes little and lasts long, and what changes quickly
After writing the replt, I realized I was being too critical of formal verification. I think Jane Street's argument holds for invariants inside code. However, I am cautious about whether that logic can be extended to other fields. I haven't studied deeply enough, so my thinking may be shallow. Please understand
You have to see it from janestreet's perspective. They're an HFT and trading high volume (millions if not 10's of millions) of stock & instruments. There is no "fix". By the time you understand what's wrong you've lost billions.
So yeah - offensive may work in non-critical areas.
Fwiw - you already use defensive everywhere. Python, Java, etc. come with garbage collectors. It's verified that the code is executing your intent.
I was wondering when we would start seeing formal verification. It makes sense that we would go from worrying about implementation details to a scientific/mathematical description of the problems.
>Fwiw - you already use defensive everywhere. Python, Java, etc. come with garbage collectors. It's verified that the code is executing your intent.
Sort of. Garbage collectors can be fallible too, especially where release optimization is used.
>Now, since it's impossible to code review the tens of thousands of lines of code that AI produces
I would simply not ask the AI to write me more code until I'm satisfied with the code it's already written! But it is true there's more of an opportunity to let the thing rip if you can give the harness the ability to meaningfully verify its own work.
> these kinds of methodologies seem like a luxury
Absolutely. The article acknowledges this. Jane Street is pretty uniquely equipped to benefit from this.
> I have to rely on machine translation to understand English documents that have no translation. The materials in my language are about 5 to 6 years behind.
Pretty much off topic, but I strongly recommend you learn English. It takes a little bit of effort, but getting rid of that constant translation overhead will be an enormous boost for you.
guy's korean, looks like? korean <-> english is the hardest language pair of two industrialized-nation languages, almost.
I don't understand the point of your comment here. Yes of course JaneStreet published that since its relevant to them. Yes, it doesn't generally apply to all programming. How is you being a "social loser" or not following these practices in your career relevant to this?
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.
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
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.
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.
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
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
Thanks! I will make sure to read the last book thoroughly. Have a good day