> I feel that when you formally verify one condition, verification of another condition gets weakened
In standard formal verification there is no problem here: you formally verify the composite "condition_1 AND condition_2"
The main point is not that everything is solved if you specify all the conjunction conditions and prove that those conjunction conditions are correct. Rather, the key point is that in that process, the agent keeps expanding subgoals.
For example, two proofs, P1 and P2, are carried out, but they proceed in a way that diverges from the actual progress of the work. That is, you can prove things like "P1: the chicken is safe" and "P2: the origin of this sauce is trustworthy," but combining these does not make a chicken dish.
In other words, the proof logic holds, but my actual task doesn't get solved. I'm questioning how to solve this problem. It's frustrating that I'm not a native English speaker at times like this. I'm sorry for causing a misunderstanding.
For example, it goes like this.
I proved P1 and P2. But then it creates P1.1. It goes and finds information from an agency certifying that this chicken is safe, and puts that in. Then it starts creating P2.1 as well. The origin of this sauce is trustworthy, but maybe there’s a better one somewhere?
It goes on like that.
Other people say that when they do AI coding, they finish quickly, but for me it’s painful because I keep having to verify it myself.
Then it should implement the whole UML skeleton, right? But it goes like this: halfway through, at some point, it says, “This algorithm is too slow? Hmm... I need to make it faster,” and tries local optimization, so sometimes I don’t get the result I want—that is, an MVP that at least runs.
I know the overall goal clearly, but there’s a problem where it gets obsessed with a specific subgoal or keeps expanding that subgoal.
AI understands "negative constraints" very well and so you should explicitly tell it "what not to do" at every stage as much as possible.
Use Top-Down and Stepwise-Refinement methodology to first generate the "Interface" and then the "Implementation" like so;
1) Ask it to produce only the "Skeleton App with well-defined Interfaces" directly 1:1 from the UML with stubs/mocks. It maybe better to use UML in text form which will allow you to annotate it easily with hints/notes for AI. The "Skeleton App" should include a) System Modules with narrow public interfaces like LKM/ioctl b) Directory structure with one module per subdirectory as a DAG with no cycles c) Explicit list of third-party libraries/frameworks to be used d) Classes/Abstract/Interfaces e) Free Functions and Class Methods with full type signatures etc.
2) Check the above and iterate until you have the UML and generated code synced up at the sufficient level of detail of Interfaces you are comfortable with. This should be compilable and is your absolute baseline which cannot be changed until you get a functional MVP.
3) Using the above skeleton, with strictly no change to any interfaces, ask it to fill in only the implementations the simplest possible way (i.e. "naive" linear, brute force etc.) with no optimizations whatsoever. Here you explicitly ask it to add runtime assertions for preconditions/postconditions/invariants. Make explicit that assertions should not have any side-effects whatsoever. This should now compile to give you the "naive" MVP.
4) Generate comprehensive test suites and test the above.
5) Now have it optimize everything, without changing the interfaces and assertions, but honouring them strictly. Compile and test against the above test suites. This should give you the "optimized" MVP.
6) Once the above passes, if performance is critical, have it comment out all assertions except "preconditions"; leave this in always. This is the minimal "sanity check".
7) Finally, for every "usecase" (i.e. feature) in the UML, have it generate the control flow graph annotated with preconditions/postconditions/invariants (which form the specification) from the previously generated code individually one per usecase. This is your "whitebox" verification documentation to make sure the implementation call graph satisfies the usecase i.e. feature specification.
Note that the above process gives you two implementations viz. the "naive" one and the "optimized" one. It is very helpful to always keep it that way as you modify/add features going forward so you can check one against the other.
You could use the same process using a textual Requirements Document etc. instead of UML. Also, if needed you can have AI generate the UML from the requirements, so you have a graphical specification of the system too.
This is the "Correctness-by-Construction" (CbC) approach using "Design-by-Contract" (DbC) methodology.
Additionally, If you generate for a strongly-typed language you can ask AI to explicitly exploit the type system fully with an eye to proving the code correct by suitable use of dependent types etc. to establish constraints for code correctness in step-1 itself as part of the interface. This is "Type-Driven Design". However, this is somewhat advanced and hence only do this if you have a good grasp of the implementation language since AI will try to be too clever and implement "typing hijinks" which can make the code incomprehensible.
Think of it as how you used wizards in older IDEs (Visual Studio MFC etc.) to first generate default skeleton app code with stubs/mocks, got it to compile and then started adding your code to it with testing and verifying at every stage. You want AI to behave in such a deterministic manner.
PS: To get started, feed my comment to AI and have it generate the necessary prompts for your AI interface ;-)
Since I’m a freelance programmer, my workflow is far removed from other people’s (there’s no review, and I mostly deliver programs based on whether they run), and I had no place to hear advice from seniors. But rramadass always helps me. Thanks to the advice you gave me, I was able to study formal verification and also study ADTs, and explore a broader world.
Some local regressions still exist, but the big looping around has decreased compared to before. It still seems long-running agents can’t fully replace humans yet. I’m always grateful, and thank you for not getting annoyed and for giving me advice even though I’m always lacking. Have a good day. Thank you so much.
May I save your comment and write it on my homepage later? Your advice seems like it will be a big help. Since I’m mostly doing things by reading manuals and books and running into problems myself, certain problems get solved quickly, but there are sections where I get stuck like this, and I always get a lot of help from you. Thank you always.
The stages in the above methodology should be expanded, which as i suggested, you can have AI do it for you. Note that you must be the "human-in-the-loop" and give the explicit go ahead after every stage i.e. checkpoint.
As part of your "Architectural Constraints", always list your specific libraries/frameworks/design patterns/code techniques that you are familiar with and want to be used while excluding everything else. For example you could say something like; "Do not use any design patterns outside of the GoF book", "Use <name> async framework only" etc. Guardrails are everything with AI.
The idea is that you should be able to read the generated code without too much difficulty.
Note that we are using DbC as one level of Formal Verification at runtime during development only. For verifying it statically we can have it mapped onto Lean4 (using tools) or to a SMT solver via SMT-LIB; see my comment here - https://news.ycombinator.com/item?id=50108112
See also; Combining Tests and Proofs with Contracts for Better Software Verification by Bertrand Meyer et al. - https://dl.acm.org/doi/10.1145/3793869
If you take a look at "real" code out there and it's evolution, you'll find that the main thing that drives it is the set of requirements. On the other side you have the platform (standard and 3rd party libraries as well as frameworks). Add to that is the set of algorithmic techniques (including design patterns).
By analyzing the requirements, you will discern that often they're composed of sub-problems that are generic (which is where you algorithms techniques comes in). And some are already solved (libraries). Often there's a common shape to the requirements (or some of them) that can be extracted into "frameworks".
So what's left then is the assembly. But often requirements are evolving concepts. So you don't want your structure (architecture) to be that rigid. You can't really know the direction of evolution, so you try to predict it in some way and add flexibility in a few places. This is more an art, but there are general techniques that works well enough.
The assembly itself is a matter of data and process. How each module is initialized, its lifecycle, which data it consumes, which data it produces. A program is always part of an information system. Means data come in, got processed, and go out. And here is the majority of development type is consumed, ensuring that the data is correctly processed.
Programming concepts like type checking, memory safety, paradigms (oop, functional, relational,...), formal verification,... are all about data. Code always come in second place. So think hard about your data and its transformation.
You have not correctly understood what i wrote.
The above is a battle-tested methodology based on experience/studies/trial-and-error and now being adapted to AI with extra tweaks. Labour which was the main bottleneck earlier is now cheap and hence we can afford to be "idealistic" since the tool is immensely powerful.
You need to expand and iterate each stage above (both individually and as a group with previous stages) in stepwise-refinement to get to what you want.
The rest of your comment is just generic platitudes and some common red herrings which i often see on HN, viz.
> main thing that drives it is the set of requirements...By analyzing the requirements,..But often requirements are evolving concepts.
Everybody just keeps parroting this without understanding. Requirements change but always in a staged manner and not willy-nilly. Hence there is always a window of time when your "Requirements Document" is frozen and you can implement a PoC/Prototype against it. The is the "naive" MVP i mention above. Later when requirements change you reiterate and regenerate your prototype and continue.
Note that the gp already had his UML design and only wanted a way to convert it to code. Hence i did not discuss requirements gathering and analysis here. Nonetheless, i had discussed this earlier in some previous comments - https://news.ycombinator.com/item?id=48274873 https://news.ycombinator.com/item?id=48264680
> Platform...libraries...frameworks...design patterns...
These are all covered under (1.c) above where you explicitly list out what to use and what not to use. These are all part of the "architectural constraints".
> So what's left then is the assembly...So you don't want your structure (architecture) to be that rigid. You can't really know the direction of evolution, so you try to predict it in some way and add flexibility in a few places. This is more an art, but there are general techniques that works well enough.
This is covered under (1) above where i enforce rigid adherence to "modularity" and "separation of concerns" by making each module's public interface narrow and extensible (eg. ioctl like) and its parameters future-proof by using versioned struct/class inheritance (eg. sockaddr). These are all well-known code patterns used in OS implementations/libraries.
> The assembly itself is a matter of data and process. How each module is initialized, its lifecycle, which data it consumes, which data it produces.
This is taken care of by having modules follow the LKM model with ioctl interface as explained above.
> Programming concepts like type checking, memory safety, paradigms (oop, functional, relational,...), formal verification,... are all about data. Code always come in second place. So think hard about your data and its transformation.
DbC methodology is the quintessential "data-driven" programming since the pre/post/inv are predicates to establish sets of data values on which the subsequent code can operate safely i.e. DbC establishes the data path for the code.
This labour was not the main bottleneck. I’m ready to bet that coding is a small part of the daily activities of a dev.
> Later when requirements change you reiterate and regenerate your prototype and continue.
That is incredibly wasteful. Requirements are set agains a world model that always evolves against its own set of constraints. Which does ties into the flexibility argument. No need to reinvent the wheel, when only a few things varies and some just stay true for years and decades..
>> The assembly itself is a matter of data and process. How each module is initialized, its lifecycle, which data it consumes, which data it produces
> This is taken care of by having modules follow the LKM model with ioctl interface as explained above.
Nope, it’s not. This is related to having a good mental model of how your software process data, not related to how you design your interface.
—-
As I said, your comments put “code” as a first place citizen, which no experience dev does. What I argue about is that it’s always about data, the rules that it follow, which will then be realized by code.
> DbC methodology is the quintessential "data-driven" programming since the pre/post/inv are predicates to establish sets of data values on which the subsequent code can operate safely
Like the one above. You don’t write code and assert which type of data that it can handle. That’s a fool errand as the outside world is naturally messy. You define the data first, and then write the code. Meaning when the data changes, the code needs to evolve. You need to have a very good mental how that changes propagate, which you won’t have of you just regenerating code.
That’s why no one builds a factory to produce factories. Although there are common elements, a factory is designed for the product it will create. So you start from the product, you don’t start from the factory. Your methodology is a framework for building factories, but with no mention of any product.
Labour doesn't mean just "typing", that is your misunderstanding. It means bringing various facets of design together to produce the final code artifact viz. main logic, typing concerns, correctness concerns, exception handling, design/code patterns, elegance, simplicity etc. It is the "cognitive load" that becomes too much. AI frees me up from thinking about all the minutiae but know enough to give instructions which can be followed and later verified. Read Dijkstra's "The Humble Programmer" to understand what i mean.
> That is incredibly wasteful. Requirements are set agains a world model that always evolves against its own set of constraints. Which does ties into the flexibility argument. No need to reinvent the wheel, when only a few things varies and some just stay true for years and decades.
Again a misunderstanding. Fred Brooks said "Plan to throw one away; you will, anyhow". That is exactly what a Prototype/PoC/"naive" MVP is. That doesn't mean you need to throw away everything everytime, it means for complex projects your prototype is often the first time that you have sorted out your requirements, design problems and satisfactorily validated your architecture. Sometimes you have to "throw one away" and restart but usually the product is always evolved (i.e. Product Families, Software Factories etc.) and almost never thrown away completely. That is what design is all about and which the above workflow accommodates. This is standard Software Engineering.
> Nope, it’s not. This is related to having a good mental model of how your software process data, not related to how you design your interface.
Whut? Designing a concrete Interface implies you have sorted out the mental model of how the software structures and processes data. That is why you verify the skeleton app design interfaces w.r.t. your requirements. This is just design philosophy 101. The details of how to drive AI to do this is in your prompt using "architectural constraints", pointers to specific libraries/frameworks/patterns etc.
> As I said, your comments put “code” as a first place citizen, which no experience dev does.
No, it does not, this is your fundamental misunderstanding.
> What I argue about is that it’s always about data, the rules that it follow, which will then be realized by code.
This is just generic platitude but nevertheless taken care of in the workflow above. You allow the tool to do it but with strict guardrails in place. It is manifested in the final approved prototype.
> You don’t write code and assert which type of data that it can handle. That’s a fool errand as the outside world is naturally messy. You define the data first, and then write the code. Meaning when the data changes, the code needs to evolve. You need to have a very good mental how that changes propagate, which you won’t have of you just regenerating code.
This is a fundamental misunderstanding of how DbC works. DbC assertions establish pre/post/inv predicates which define subsets of the program "state space". This means you know the function signature i.e. the types/ranges-of-objects on which you will operate and are establishing their safe subsets within which the code shall operate. You first write the pre/post/inv and then write code to satisfy the constraints. See articles on DbC by Bertrand Meyer given here - https://news.ycombinator.com/item?id=48358691
> That’s why no one builds a factory to produce factories. Although there are common elements, a factory is designed for the product it will create. So you start from the product, you don’t start from the factory. Your methodology is a framework for building factories, but with no mention of any product.
The product is specific to your problem domain and your understanding of it. The above problem-solving workflow can be applied to generate requirements artifacts for a product instead of code if needed. It is a general meta-methodology which you can adapt for any purpose using AI. The stages are just checkpoints to ensure that AI is always under your control i.e. behaves deterministically. As an example, there are now a whole bunch of startups focusing on just "Requirements Modeling", "Specification Driven Development" etc. to structure ambiguous product requirements so that AI does exactly what you want it to do.
So you can get AI to produce code, but you should refine your mental model alongside it and not try to build a scaffold as that would always be too generic and wrong. As a scaffold good enough is already code. So exoskeletons mindset, more than hive mindset.
I suspect your confusion lies in not looking at the end-to-end aspects of Software Engineering and only focusing on local aspects of Design.