4 ms·

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,

by jdw64 5mo ago

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.

stephenlf 5mo ago
> these kinds of methodologies seem like a luxury Absolutely. The article acknowledges this. Jane Street is pretty uniquely equipped to benefit from this.
ngruhn 5mo ago
> 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.
- jdw64 5mo ago
  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
  - majormajor 5mo ago
    > 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.
    - jdw64 5mo ago
      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
orochimaaru 5mo ago
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.
- coderenegade 5mo ago
  >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.
altmanaltman 5mo ago
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?
teiferer 5mo ago
> 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.
- curuinor 5mo ago
  guy's korean, looks like? korean <-> english is the hardest language pair of two industrialized-nation languages, almost.
rramadass 5mo ago
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 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-methods-informally/4DE900050EB3C855E4BB627A94B4176E#overview 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_correspondence 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 5mo ago
  I'm sorry, but what you've said are things I've already read.(this:https://research.tue.nl/en/publications/on-formal-methods-thinking-in-computer-science-education/ 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.
closeparen 5mo ago
>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.

by jdw64 5mo ago

stephenlf 5mo ago

> these kinds of methodologies seem like a luxury Absolutely. The article acknowledges this. Jane Street is pretty uniquely equipped to benefit from this.

ngruhn 5mo ago

> 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.

jdw64 5mo ago
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
- majormajor 5mo ago
  > 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.
  - jdw64 5mo ago
    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

orochimaaru 5mo ago

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.

coderenegade 5mo ago
>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.

altmanaltman 5mo ago

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?

teiferer 5mo ago

> 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.

curuinor 5mo ago
guy's korean, looks like? korean <-> english is the hardest language pair of two industrialized-nation languages, almost.

rramadass 5mo ago

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 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-methods-informally/4DE900050EB3C855E4BB627A94B4176E#overview 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_correspondence 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 5mo ago
I'm sorry, but what you've said are things I've already read.(this:https://research.tue.nl/en/publications/on-formal-methods-thinking-in-computer-science-education/ 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.

closeparen 5mo ago

>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.