rramadass

Your problem is that you have not established "guardrails" for the AI and so it goes off and tries to do everything it can to help you (its default persona is "people pleaser").

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 ;-)

Very Interesting!

Do you have a detailed paper/article written on this?

> I think the royal combo is Lean 4/TLA+/etc. plus AI plus a deterministic generator. For large systems formal method assertions need to be compressed down to a human comprehensible size. This can happen when the assertions are confirming the accuracy of a model and its attached code generators. The generator can generate proofs of the generated code and a human only needs to ensure that the generator provably generates the correct mass scale assertions.

This is not completely clear; would you mind elaborating on that in more detail?

Both of you are right in slightly different senses.

There is no "global time clock" and hence in a philosophical sense there is no "common now".

However, the speed of light is constant in the universe and so you can calculate time based on distance traveled by light to you provided you are not moving at speeds comparable to speed of light. This means you can suppose a "common lightyear clock" for measurement.

But when the speeds are comparable to that of light, you have time dilation and length contraction and so even the "common lightyear clock" is invalid. This is the principle of "Relativity of Simultaneity".

The way to think about it is, Events happen in a Space-Time fabric and so in order to measure the interval between two events you have to consider both Space and Time w.r.t. object speed vs. speed of light. The universal invariant here is the "Space-Time Interval" between two events which will be the same for everybody whatever be their mass or speed.

Mandatory Background:

1) Understanding Formal Methods by Jean-Francois Monin - This is the absolute best for getting a grip on the breadth, concepts and sample tools for Formal Mathematics/Specification/Verification. Fire-hose of information (not a step-by-step textbook) so use this as a map for everything "Formal". The S/N ratio is very high (~250 pages only!) so use AI/Textbooks to help explain concepts you find difficult to understand.

Practical:

1) Software Abstractions: Logic, Language, and Analysis by Daniel Jackson - Uses "Alloy" language to teach Structural (i.e. Data) Modeling.

2) Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers by Leslie Lamport - Uses "TLA+" language to teach Behavioural (i.e. State Machine) modeling.

The above two are for "System Modeling" i.e. everything needed to formally build complete systems.

3) Finally, You should also look at the bunch of free books on the Lean4 website which can be studied parallely for "code-level" proofs and verification.

PS: There are a few more (eg. Event-B method etc.) but you can get to those if/when you need to.

Yep, i have read versions of this story earlier, i think in one of the martial arts tales books by Pascal Fauliot.

PS: My HN handle is based on my real name and not because i am a follower of "Ram Dass" (American) ;-)

The frenchman line does not occur in other editions of this essay. This is the only place i have seen it.

The essay itself is highly thought-provoking and an evisceration of Mankind. I especially like his indictment of "Moral Sense";

One is obliged to concede that in true loftiness of character, Man cannot claim to approach even the meanest of the Higher Animals. It is plain that he is constitutionally incapable of approaching that altitude; that he is constitutionally afflicted with a Defect which must make such approach forever impossible, for it is manifest that this defect is permanent in him, indestructible, ineradicable.

I find this Defect to be the Moral Sense. He is the only animal that has it. It is the secret of his degradation. It is the quality which enables him to do wrong. It has no other office. It is incapable of performing any other function. It could never have been intended to perform any other. Without it, man could do no wrong. He would rise at once to the level of the Higher Animals.

Since the Moral Sense has but the one office, the one capacity -- to enable man to do wrong – it is plainly without value to him. It is as valueless to him as is disease. In fact, it manifestly is a disease.

The Moral Sense enables a man to do wrong. It enables him to do wrong in a thousand ways. Rabies is an innocent disease, compared to the Moral Sense. No one, then, can be the better man for having the Moral Sense. What now, do we find the Primal Curse to have been? Plainly what it was in the beginning: the infliction upon man of the Moral Sense; the ability to distinguish good from evil; and with it, necessarily, the ability to do evil; for there can be no evil act without the presence of consciousness of it in the doer of it.

The point is that moral sense enables one to distinguish right from wrong and so when you do wrong to others you are fully conscious of the suffering it causes. And yet mankind does it in a thousand different ways.

The main reason is the insane levels of pollution in Indian urban centers which is literally in your face everywhere. Hence everybody is very much conscious of EV adoption (a necessity) and are transitioning to them as soon as they are available and affordable.

If the Chinese and Indian govts. sort out their differences allowing their EV companies to better share technologies and production, thus bringing prices down drastically, the entire planet's environment will be changed!.

The US/Europe are being absolutely moronic when it comes to EV vehicles.

Their core technology (batteries, inverters, electric motors, drive trains, thermal management, software etc.) are all pretty similar (not too much essential variation) across brands and hence the main differentiator becomes price and cosmetics.

In the developing world cost is king, you don't need too much power, smaller size, maneuverability and comfort are the key parameters. Their EV market is for the taking and China is doing it easily with US/Europe not even in the race.