Code Review Starts with What Must Stay True
Software development has long assumed that people will read and understand the code. We choose clear names and break up long functions so that the next person can follow our intent.
But when AI produces code continuously, human reading speed becomes a bottleneck. Reviewing a change means looking beyond the diff: surrounding logic and existing requirements matter too. The amount we need to read keeps growing.
We need a way to observe code. Start by deciding which properties a change must preserve, then extract the information needed to check them. The aim is to judge a change by what it preserves and what it alters, without requiring someone to read the entire implementation.
Express the properties you care about as Laws
A Law states a property we want software to satisfy: how it should behave, how it should be structured, or what should remain true after a change.
Specifications describe behavior. Design rules constrain structure and dependencies. Compatibility requirements identify behavior that must survive a change. All express something we want to be true of the software. Laws generalize these different requirements so we can work with them in a common framework.
Once the subject and conditions are clear, familiar requirements can be written as Laws.
| Where the requirement comes from | Property to preserve | What to examine |
| --- | --- | --- |
| Functional specification | Create order lines in basket order | The code that creates order lines |
| Design rule | The UI layer must not call the persistence layer directly | Calls and layer membership |
| API compatibility policy | Preserve existing response fields after a change | Response definitions before and after the change |
| Business rule | A refund must not exceed the amount paid | The relationship between payment and refund amounts |
Define an Atom vocabulary for checking those Laws
To check a Law, we need to decide what to look for in the code and how to record it. Atom definitions provide that vocabulary. Each fact we extract is recorded as an Atom using those definitions.
For “the UI layer must not call the persistence layer directly,” we record who calls whom and which layer each belongs to. For order-line sequencing, we record the kind of operation and its processing order. The same code calls for different observations depending on the property we want to check.
An ArchMap collects the facts extracted from the code in this vocabulary.
| Element | Role |
| --- | --- |
| Law | States a property the subject must satisfy |
| Atom definitions | Define the kinds of subjects and values we can record |
| ArchMap | Records observed facts in that vocabulary, with references to the source |
We ask AI to observe the code, then check whether the values in the ArchMap satisfy the Laws.
The Law and Atom vocabulary is independent of any particular language or framework. If we define operations by their meaning, such as “create an order line” or “allocate stock,” we can use the same Laws for Python and Java implementations. AI reads each implementation and records what it finds in the shared vocabulary.
It can also interpret what a piece of code does in business terms. It might follow a sequence of calls across several functions and record, “this is where stock is allocated.” Observations can include meaning that is difficult to capture from syntax and type information alone.
A real example: fixing stock allocation changed the display order
django-oscar, an e-commerce framework built with Python and Django, has a useful example of a stock-allocation change affecting the order in which purchased items appeared.
When an order is placed, the application creates order lines from the basket and allocates stock. Originally, both operations ran in one loop. In pseudocode:
for line in basket_lines:
create_order_line(line)
allocate_stock(line)
A change introduced a consistent processing order for stock allocation. The aim was to acquire stock locks in the same order when multiple orders were placed concurrently. Basket lines were sorted by their stock records before entering the loop:
for line in sort_by_stockrecord(basket_lines):
create_order_line(line)
allocate_stock(line)
This aligned the stock-allocation order. It also changed the order in which order lines were created, because both operations were still in the same loop.
Suppose a basket contains a notebook followed by a pen, but their stock records sort in the opposite order. The code now creates the pen's order line first. Since django-oscar retrieved order lines in primary-key order, the change affected how items appeared in order details, invoices, and emails.
Write down the two Laws
There are two properties to check:
| Law | Property |
| --- | --- |
| L1 | Allocate stock in stock-record order |
| L2 | Create order lines in basket order |
L1 is what the change is meant to achieve. L2 is what it must preserve.
Ask AI to extract the operations and their order
To check these Laws, we need the kind of each operation and the order in which it runs. We define the following Atom fields:
| Field | What to record |
| --- | --- |
| kind | Order-line creation or stock allocation |
| sequence | Basket order or stock-record order |
| loop | Which loop contains the operation |
Recording loop also helps explain why the two operations were reordered together.
I gave AI these definitions and Laws and asked it to read the code before and after the sorting change. The resulting ArchMap contained these observations:
| Version | Operation | Order | Loop |
| --- | --- | --- | --- |
| Before the change | Create order line | Basket order | 1 |
| Before the change | Allocate stock | Basket order | 1 |
| After sorting | Create order line | Stock-record order | 1 |
| After sorting | Allocate stock | Stock-record order | 1 |
The ArchMap also records source locations, so a value can be checked against the code it came from.
Check both Laws with ArchSig
ArchSig is a tool under development that checks observed information against Laws. Passing the Atom definitions, Laws, and ArchMaps to v0.6.0 produced these results:
| Version | L1: allocate in stock-record order | L2: create order lines in basket order |
| --- | --- | --- |
| Before the change | Not satisfied | Satisfied |
| After sorting | Satisfied | Not satisfied |
The stock-allocation order was fixed, but the order-line sequence changed with it. An effect that is easy to miss when reviewing only the intended fix becomes something we can explicitly check once the property is written as a Law.
Split the loop to satisfy both Laws
The observations show that both operations are in the same loop. That is why changing the stock-allocation order also changed order-line creation. Splitting the loop lets each operation use the order it needs:
for line in basket_lines:
create_order_line(line)
for line in sort_by_stockrecord(basket_lines):
allocate_stock(line)
This is also how django-oscar was fixed. PR #4594 introduced the stock-ordering change; PR #4598 separated the loops.
Observing the repaired code with the same fields gave:
| Operation | Order | Loop |
| --- | --- | --- |
| Create order line | Basket order | 1 |
| Allocate stock | Stock-record order | 2 |
Checking this ArchMap showed that both L1 and L2 were satisfied. Stock allocation now followed the required order, while order lines still followed the basket.
Treat specifications and conventions as properties to preserve
This example brings together an internal requirement about stock processing and a user-visible requirement about display order. Software also has design rules, compatibility commitments, and business rules. Some live in specifications; others are conventions shared by the team.
Thinking of all of them as properties to preserve lets us put them on the same list of things to check after a change. That is the value of generalizing them as Laws: we can consider what we want to fix alongside what we need to keep.
For each requirement, ask what must be true, and of what. The information needed to check it becomes clearer. Laws turn specifications and conventions into questions we can investigate in the code.
Treat Laws as equations and explore the solution space
If a Law is not satisfied, what should change? Expressing Laws as equations lets us look for repairs among their solutions. Software that satisfies several Laws at once can be viewed as a solution to a large system of simultaneous equations.
Let \(x\) be a tuple of variables, and express the Laws as:
$$
f_1(x)=0,\quad f_2(x)=0,\quad\ldots,\quad f_m(x)=0.
$$
The tuples satisfying every equation form a solution set:
$$
\mathcal S={x\mid f_1(x)=\cdots=f_m(x)=0}.
$$
Diagnosis asks whether the current values belong to \(\mathcal S\). If they do not, we can search within \(\mathcal S\) for a state to move to. The same Laws support both finding a problem and repairing it.
Each equation narrows the choices
Take two rational-valued variables, \(u\) and \(v\), and one equation:
$$
u+v=2.
$$
There are infinitely many solutions, including \((u,v)=(0,2),(1,1),(2,0)\). In general, a solution has the form \((t,2-t)\), with \(t\) free to vary.
Now add \(u-v=0\):
$$
\begin{cases}
u+v=2,\
u-v=0.
\end{cases}
$$
Adding the equations gives \(2u=2\), so the solution is uniquely \((u,v)=(1,1)\). If we also require \(u=0\), no solution satisfies all three equations.
View the solutions geometrically
Treating the variables as coordinates gives the solutions a geometric shape. The equations \(u+v=2\) and \(u-v=0\) describe lines, and \((1,1)\) is their intersection. Each additional equation narrows the candidates to points satisfying all the conditions.
Algebraic geometry develops this idea using polynomials and rings. Specifying the values, operations, and relations lets us study spaces of solutions and maps between them.
Algebraic Architecture Theory (AAT) brings this approach to software structure. It constructs Law equations and solution spaces from data describing states and operations. Studying these spaces gives us a way to reason about diagnosis, change, and repair. ArchSig applies this theory to software analysis.
The allowed changes determine where we can search
A repair does not necessarily allow every variable to change. Let \(x_0\) be the current state, and let \(\mathcal A(x_0)\) contain the states reachable through permitted changes. A repair candidate must also satisfy the Laws, so it lies in:
$$
\mathcal A(x_0)\cap\mathcal S.
$$
If this intersection is empty, the permitted changes cannot produce a repair. Otherwise, its elements are candidate repaired states.
The system above had the solution \((1,1)\). Starting from \((0,2)\), we cannot reach it if \(u\) must stay at zero and only \(v\) may change. If both can change, we can choose \((1,1)\). Whether a repair exists depends on what we are allowed to change, even when the Laws stay the same.
Build one structure from Atoms and Laws
AAT brings Atoms and Laws together with the available operations and the relationships between parts. Its distinguishing idea is to use this common structure for diagnosis, repair, and comparison of changes. The foundations are developed in Foundations of Algebraic Architecture Theory: A Rising Sea of Geometry, Transport, Comparison, and Reconstruction.
Bring facts, operations, and conditions together
AAT starts mathematically from Atoms. Giving relationships to Atoms that represent components and operations lets us treat a software structure as a mathematical object. Laws specify the equations that object must satisfy.
We also include the allowed operations and the states they can produce. This lets us ask whether Laws still hold after an operation and what is preserved by a change.
To study a large object in parts, we specify the parts and what they share. We include the data for each part and how discrepancies between parts are measured. The paper calls the resulting structure a full geometry.
Use the same structure to ask different questions
Several familiar software questions can then be studied within that structure:
| Software question | Mathematical question |
| --- | --- |
| Can individually correct parts conflict when combined? | Can local states be glued into a global state? |
| Can we omit detail and still detect the same problems? | Is diagnosis preserved when the reading changes? |
| Do different orders of changes or migration paths remain consistent? | Do the structures and operations obtained along different paths correspond? |
| What changes preserve the requirements? | Can we classify structure-preserving maps? |
| Can descriptions from separate teams determine the overall design and its changes? | Can we reconstruct objects and maps from local data? |
For example, suppose we want to change a data format while keeping the same operations available. Let \(X\) and \(Y\) be the objects before and after conversion, \(h\) the conversion map, and \(T_X,T_Y\) the respective operations. We can express the required relationship as:
$$
h(T_X(x))=T_Y(h(x)).
$$
Operating and then converting must give the same result as converting and then operating. We can check not just that values correspond, but that the conversion respects the operations on them.
When can we omit detail without changing the diagnosis?
Call a way of extracting information from an object a reading. A reading can omit detail and still be sufficient to evaluate a Law. Combining cases without retaining every distinction is called coarse-graining.
But if an object satisfying the Law and one violating it produce the same observation, we have discarded information we needed.
Can the observation alone determine whether the Law holds?
Let \(x\) be an object, \(q\) a reading, and \(L\) the evaluation of a Law. If \(\bar{L}\) evaluates the Law using only the observed information \(q(x)\), we need:
$$
L(x)=\bar{L}(q(x)).
$$
The observed information must give the same evaluation as examining the whole object.
Suppose \(x=(u,v)\) and we observe only \(q(u,v)=u+v\). That is enough to decide whether \(u+v=2\). It is not enough to decide whether \(u=v\): both \((0,2)\) and \((1,1)\) produce an observation of 2, but only the latter satisfies \(u=v\).
The same principle applies to software. To check that the UI layer never directly calls the persistence layer, call relationships and layer membership are enough. We do not need to inspect every calculation inside those functions. But that information cannot tell us whether a refund exceeds the payment. Choosing the Law first helps us decide what we can leave out.
The Atlas theorem connects observation detail to diagnosis
Some discrepancies between parts can be removed by adjusting the values in each part. Others remain. Cohomology captures this distinction, with persistent discrepancies represented by obstruction classes.
Consider discrepancies between three parts, A, B, and C. Suppose they sum to 1 when followed around the cycle from A to B, B to C, and C back to A.
Adjust the values at the three parts by \(u_A,u_B,u_C\). The discrepancies on the edges change by \(u_B-u_A\), \(u_C-u_B\), and \(u_A-u_C\). But those adjustments sum to zero:
$$
(u_B-u_A)+(u_C-u_B)+(u_A-u_C)=0.
$$
Adjusting the individual values changes the discrepancies along the edges, but not their sum around the cycle. The original discrepancy of 1 remains: these adjustments cannot remove it.
The Atlas theorem gives conditions under which these persistent discrepancies correspond between a detailed reading and a coarser one. Both readings must support evaluation of the Laws, and the overlaps between parts and the calculations of discrepancies must correspond as well. Under those conditions, omitting detail neither hides an obstruction nor creates an extra one.
Suppose we want to examine a large codebase at module level rather than function level. If that grouping satisfies the Atlas conditions, it preserves the diagnosis of discrepancies for the Laws being studied. We gain a basis for deciding how much to inspect: this information is enough for this diagnosis.
Local repairs do not automatically fit together
When a large system of equations is split into parts, each part may have a solution without those solutions fitting together. Shared variables must agree.
Suppose one part solves \(u+v=2\) and chooses \((u,v)=(0,2)\). Another solves \(v+w=3\) and chooses \((v,w)=(1,2)\). Both satisfy their own equations, but they disagree on \(v\), so they cannot form a single solution. Keeping the first solution, we can choose \((v,w)=(2,1)\) for the second and obtain the global solution \((u,v,w)=(0,2,1)\).
Combining local solutions that agree on their shared parts is called gluing. AAT uses sheaves and cohomology to study gluing and the discrepancies that obstruct it.
SAGA: use equations to find what prevents a repair
Solving equations changes variable values. Repairing software changes settings or structures through permitted operations. To use a calculation for repair, we must connect those operations to changes in values.
The SAGA comparison theorem connects obstructions constructed from repair operations with obstructions constructed from equations. When that correspondence meets the theorem's conditions, we can use the equations to determine whether an obstruction to repair remains.
For example, several services might each admit a fix, yet disagree about shared data or configuration. Those fixes cannot all be applied together. Once the permitted repairs and shared conditions are represented by the corresponding equations, a nonzero obstruction means the repairs cannot be made compatible within those operations. With the additional gluing conditions in place, a zero obstruction means a compatible global repair exists.
Ariadne: find a repair within the allowed scope
Ariadne lets us specify what may change and what must stay fixed. It asks whether a repair is possible within that scope and finds candidates when it is.
Suppose two parts share a correction \(u\). One requires \(u=x\), and the other requires \(u=y\), where \(x,y\) are given target values:
$$
\begin{cases}
u=x,\
u=y.
\end{cases}
$$
A solution exists only when \(x=y\). Subtracting the first equation from the second leaves zero on the left and \(y-x\) on the right. If that difference is nonzero, no choice of \(u\) can repair the system.
Now allow an additional correction \(v\) in the second part:
$$
\begin{cases}
u=x,\
u+v=y.
\end{cases}
$$
We can choose \(u=x\) and \(v=y-x\). Broadening the allowed changes makes the target reachable.
Ariadne works with finite linear models, constructing repairs from the conditions on each part. When repair is impossible, it identifies what prevents it.
Software fixes often have constraints such as “leave the shared configuration unchanged; modify only this service's settings.” If the settings and Laws can be expressed in this model, we can determine whether that scope admits a repair before repeatedly trying patches. If it does, we can compute candidate values. If it does not, we can broaden the scope, perhaps allowing changes to shared configuration, and check again.
Observe the information needed for a concrete repair
The system with the additional correction \(v\) has a solution for every \(x,y\). We can therefore answer “a repair exists” without knowing their values. Returning actual values for \(u,v\), however, requires knowing \(x\) and \(y-x\).
Deciding whether a solution exists and producing one require different information. If we read \(x\) and \(y\) separately, we need both values. If \(x\) is already known, only \(y\) remains to be observed.
If choosing a repair requires a missing configuration value, we can ask AI to inspect that configuration. The repair equations can also guide what to observe next.
Reconstruct the whole from local descriptions
When work on a large codebase is divided among several people or agents, we may want to assemble an overall structure or change from their separate descriptions.
The local reconstruction theorem in the Rising Sea paper gives conditions for doing this. Local descriptions include operations, Laws, and agreement on shared parts, alongside information about individual components. When the required conditions hold, we can reconstruct both the overall structure and changes that preserve it.
Suppose several AI agents investigate different modules and propose changes. We put their descriptions into the form required by the theorem and check that shared parts agree and operations correspond. If the conditions hold, their local changes can be assembled into a global change. We can ask whether proposals that look reasonable individually actually fit together.
This ability to address diagnosis, repair, comparison of changes, and reconstruction through a common structure built from Atoms and Laws is AAT's central strength.
Connections to formal verification and development with proofs
Making desired properties explicit and checking them is also central to formal methods such as TLA+ and Alloy. TLA+ describes system behavior in specifications whose properties can be checked through model checking and proof. Alloy describes relations and constraints, then searches for satisfying examples or counterexamples to properties. When these models are written separately from the implementation, keeping the two aligned as code changes takes work.
Bend 2 takes an approach in which rules and their proofs are written alongside the code. Rules are declared as laws, and the compiler checks their proofs.
A strength of applying AAT through ArchSig is that source code remains the single source of truth about the implementation, with diagnosis added afterward. Desired properties are written as Laws; the state of the implementation is observed from the current code. An ArchMap can be regenerated with each observation, so it need not be maintained by hand in parallel with the code.
AI can keep writing code while we observe and diagnose it at the points we choose. Each implementation change need not wait for a separate model or proof to be completed. This lets us check changes while retaining the speed of AI-assisted development.
Rice's theorem establishes a limit on automatic analysis. Consider a property of the function a program computes. If some programs satisfy it and others do not, no algorithm can always terminate and correctly decide that property for every program. That makes the choice of Laws and models important. Within a suitable finite model or a system of linear equations, we can compute diagnoses and repairs for that scope.
From reading code to observing it through Laws
The next step I want for ArchSig is to let users specify what may change, then find candidate repairs that satisfy the Laws within the model. If no candidate exists, the tool should identify what prevents one. If information is missing, AI can read the relevant code or specification. We can then apply a candidate to the code, observe it again, and test the result.
Where several candidates exist, people can choose among them based on performance, maintainability, and the cost of migration.
The starting point is to write down what must remain true after a change. Express it as Laws, ask AI to extract the information needed to check them, and use mathematics to reason about diagnosis and repair. That is the kind of development I want to make possible: judging changes without depending on someone reading every line.
---
Repository: AlgebraicArchitectureTheoryV2
1 reaction
守りたい性質からはじめるコード観測
これまでのソフトウェア開発は、人がコードを読んで理解することを前提にしてきました。分かりやすい名前を付け、長い処理を分けるのも、読む人が意図を追えるようにするためです。
しかし、AIが次々にコードを書くようになると、人が読む速度では追いつきません。変更された箇所だけでなく、周囲の処理や既存の仕様まで確かめようとすれば、読む量はさらに増えます。
これからは、コードを観測するという考え方が必要です。まず、変更後も守りたい性質を決めます。そして、それが保たれているかを確かめるために、必要な情報をコードから取り出します。すべてを人が読み通さなくても、何を守り、何が変わったかをもとに判断できるようにしたいのです。
守りたい仕様や規約を、Lawとして書く
Lawは、ソフトウェアに求める性質を表すものです。どのように動いてほしいか、どんな構造であってほしいか、変更しても何を保ちたいかを書きます。
仕様はソフトウェアの振る舞いを、設計規約は内部の構造や依存関係を定めます。互換性を守るには、変更前のどの振る舞いを残すかを決めます。いずれも「ソフトウェアにこうあってほしい」という要求です。Lawは、こうした仕様や規約を一般化し、同じ枠組みで扱うためのものです。
対象と条件をはっきりさせれば、身近な仕様や規約もLawとして書けます。
要求の出どころ
守りたい性質の例
確認する対象
機能仕様
注文行はカゴの行順に作る
注文行を作る処理
設計規約
UI層から永続化層を直接呼び出さない
層と呼出しの関係
APIの互換性方針
変更後も既存の応答項目を保つ
変更前後の応答定義
業務ルール
返金額は支払額を超えない
支払額と返金額の関係
Lawを確かめるための語彙を、Atomとして定義する
Lawに書いた性質を確かめるには、コードの何を調べ、どんな値として記録するかを決める必要があります。そのための語彙を、Atomの定義として用意します。コードから読み取った一つひとつの事実は、この語彙を使ってAtomとして記録します。
たとえば「UI層から永続化層を直接呼び出さない」なら、誰が誰を呼び出し、それぞれがどの層に属するかを記録します。注文行の順序を確かめたいなら、操作の種類と処理順序を記録します。同じコードでも、確かめたい性質によって、調べる項目が変わります。
この語彙に沿ってコードから読み取った事実をまとめるのが、ArchMapです。
要素
役割
Law
対象が満たすべき性質を記述する
Atomの定義
対象の種類や観測する値の語彙を定める
ArchMap
その語彙に沿って観測した事実を、ソースの根拠とともに記録する
AIにコードを観測してもらい、ArchMapに記録された値がLawを満たすかを確かめます。
LawやAtomの語彙は、特定の言語やフレームワークに縛られません。「注文行を作る」「在庫を引き当てる」といった意味で定義すれば、PythonでもJavaでも、同じLawで確かめられます。AIがそれぞれの実装を読み、共通の語彙で記録するからです。
AIには、その処理が業務上何をしているかも読み取ってもらえます。たとえば、複数の関数に分かれた処理を追い、「ここで在庫を引き当てている」と記録します。構文や型の情報だけでは捉えにくい意味も、観測に含められます。
【具体例】在庫処理を直したら、商品の表示順が変わった
PythonとDjangoで作られたEC基盤のdjango-oscarに、在庫処理の修正が注文の表示順に影響した事例があります。
注文を確定するときは、カゴの商品から注文行を作り、在庫を引き当てます。もともとは、一つのループで両方を処理していました。擬似コードにすると、こうなります。
for line in basket_lines:
create_order_line(line)
allocate_stock(line)
ここに、在庫を処理する順序を揃える修正が入りました。同時に複数の注文が入っても、在庫のロックを同じ順序で取るためです。在庫情報を持つレコード（stockrecord）の順に並べ替えてから、ループを回します。
for line in sort_by_stockrecord(basket_lines):
create_order_line(line)
allocate_stock(line)
これで在庫の処理順は揃います。ところが、同じループで作っている注文行まで並べ替わってしまいました。
たとえば、カゴに「ノート、ペン」の順で入れていても、stockrecordの順序が逆なら、注文行は「ペン、ノート」の順に作られます。django-oscarでは注文行を主キー順に取得していたため、注文詳細や請求書、メールの表示順まで変わってしまったのです。
守りたいことを二つのLawにする
この修正で確認したいのは、次の二つです。
Law
守りたいこと
L1
在庫はstockrecord順に引き当てる
L2
注文行はカゴ順に作る
L1は今回の修正で実現したいこと、L2はその修正でも変えたくないことです。
AIに処理の種類と順序を読み取ってもらう
この二つのLawを確かめるために、処理の種類と順序を調べます。Atomの定義には、次の項目を用意します。
項目
読み取ること
kind
注文行の作成か、在庫の引当か
sequence
カゴ順か、stockrecord順か
loop
どのループに入っているか
loopも記録すると、二つの処理が一緒に並べ替わった理由を追いやすくなります。
AIにこの定義とLawを渡し、変更前と並べ替え後のコードを読んでもらいました。ArchMapにまとめた結果が、次の表です。
コード
処理
順序
ループ
変更前
注文行作成
カゴ順
1
変更前
在庫引当
カゴ順
1
並べ替え後
注文行作成
stockrecord順
1
並べ替え後
在庫引当
stockrecord順
1
ArchMapには元のコードの位置も記録するので、気になる値があれば該当箇所を確認できます。
ArchSigで二つのLawをチェックする
観測した情報がLawを満たすかをチェックするツールが、開発中のArchSigです。v0.6.0にAtomの定義、Law、ArchMapを渡すと、次の結果になりました。
コード
L1：在庫引当はstockrecord順
L2：注文行作成はカゴ順
変更前
満たさない
満たす
並べ替え後
満たす
満たさない
在庫の処理順は直りましたが、注文行の順序は変わってしまいました。修正の目的だけを見ていると見落としやすい影響も、守りたい性質をLawに書いておけば確認できます。
ループを分けて、両方のLawを満たす
観測結果を見ると、二つの処理は同じループに入っています。在庫引当の順序を変えたとき、注文行の作成順序も一緒に変わったのは、このためです。それぞれを必要な順序で処理するには、ループを分けます。
for line in basket_lines:
create_order_line(line)
for line in sort_by_stockrecord(basket_lines):
allocate_stock(line)
django-oscarで実際に行われた修正も、この形でした。在庫の処理順を揃えた変更はPR #4594、ループを分けた修正はPR #4598に記録されています。
修正後のコードも、同じ項目で観測しました。
処理
順序
ループ
注文行作成
カゴ順
1
在庫引当
stockrecord順
2
このArchMapをチェックすると、L1もL2も満たす結果になりました。在庫の処理順を直しつつ、注文行の順序も保てています。
仕様も規約も、守りたい性質として扱う
今回、一緒に確かめたのは、在庫処理の都合と、利用者に見える表示順でした。開発では、このほかにも設計規約、APIの互換性、業務上のルールなどを守る必要があります。仕様書に書かれているものもあれば、チームの慣習として共有されているものもあります。
こうした要求を「守りたい性質」として捉えると、仕様書にあっても慣習であっても、変更後に確かめる条件として並べられます。今回直したいことと、引き続き守ることを一緒に扱えるのが、Lawとして一般化する意義です。
それぞれの要求について「何が、どうなっていればよいか」を書くと、確認に必要な情報も見えてきます。Lawは、仕様や規約を、コードから確かめられる問いにするための考え方です。
Lawを方程式として捉え、解の空間を考える
Lawを満たしていなければ、どう変えればよいでしょうか。Lawを方程式で表すと、修復の候補をその解として探せます。複数のLawを同時に満たすソフトウェアは、大きな連立方程式の解として捉えられます。
変数の組をxとし、Lawを次の方程式で表します。
f_1(x)=0,\quad f_2(x)=0,\quad\ldots,\quad f_m(x)=0.
それぞれの式を満たす値の組を集めると、解の集合が得られます。
\mathcal S={x\mid f_1(x)=\cdots=f_m(x)=0}.
現在の値が\mathcal Sに入っているかを確かめるのが診断です。入っていなければ、\mathcal Sの中から変更先を探します。同じLawが、問題の発見にも修復にも使えます。
方程式を加えると、選択肢が絞られる
有理数を値に取る二つの変数u,vについて、まず一つの方程式を考えます。
u+v=2.
解は(u,v)=(0,2),(1,1),(2,0)など、無数にあります。一般には(t,2-t)と書け、tを自由に選べます。
ここにu-v=0を加えると、連立方程式になります。
\begin{cases}
u+v=2,\
u-v=0.
\end{cases}
二つの式を足すと2u=2なので、解は(u,v)=(1,1)に決まります。さらにu=0を要求すると、すべてを満たす解はなくなります。
解の集合を、幾何として調べる
変数を座標とみなすと、方程式の解を図形として眺められます。u+v=2とu-v=0はそれぞれ直線の方程式で、両方を満たす点(1,1)はその交点です。式を加えるたびに、それらを同時に満たす点へと候補が絞られます。
代数幾何では、この考え方を多項式や環の言葉で扱います。どの値を使い、どの演算を認め、どの関係式を課すかを定めることで、解の空間と、その間の写像を調べられます。
この考え方をソフトウェアの構造に広げるのが、AAT（代数幾何的アーキテクチャ論）です。状態や操作を表すデータから、Lawの方程式と解の空間を作ります。その空間を調べることで、診断や変更、修復を考えます。ArchSigは、この理論をソフトウェアの分析に応用するツールです。
変更の制約は、解を探す範囲を定める
修復では、すべての変数を自由に変えられるとは限りません。現在の値をx_0とし、許された変更で移れる先を集めた集合を\mathcal A(x_0)とします。その中でLawも満たすものを探すので、求める候補は次の共通部分にあります。
\mathcal A(x_0)\cap\mathcal S.
この共通部分が空なら、許された変更だけでは修復できません。空でなければ、その要素が修復後の候補になります。
先ほどの連立方程式の解は(1,1)でした。現在の値が(0,2)で、uを0に固定したままvだけ変えるなら、解には到達できません。両方の変更を許せば、(1,1)を選べます。Lawが同じでも、どこまで変更してよいかによって、直せるかどうかが変わります。
AtomとLawから、共通の構造を作る
AATでは、AtomとLawをもとに、どんな操作ができるか、部分同士がどう関わるかを一つの構造にまとめます。診断や修復、変更の比較に、同じ構造を使うのが特徴です。この基礎をまとめたのが、論文Foundations of Algebraic Architecture Theory: A Rising Sea of Geometry, Transport, Comparison, and Reconstructionです。
事実、操作、条件を一つの対象にまとめる
AATでは、Atomを数学の出発点に置きます。部品の存在や操作などを表すAtomに関係を与えると、ソフトウェアの構造を一つの数学的な対象として扱えます。その対象が満たすべき方程式をLawとして指定します。
さらに、どの操作を許し、それによってどんな状態へ移れるかも含めます。現在の状態だけでなく、操作した後もLawを満たすか、変更の前後で何が保たれるかを調べるためです。
大きな対象を分けて調べるなら、どこで分け、どこを共有するかも決めます。さらに、各部分のデータと、部分同士の食い違いをどう測るかを組み込みます。論文では、これらをまとめた構造を「完全幾何」と呼んでいます。
同じ構造から、複数の問題を考える
ソフトウェアに関するさまざまな問いを、この構造の上で考えられます。
ソフトウェアについての問い
共通の構造の上で調べること
各部分は正しくても、組み合わせると矛盾しないか
局所の状態を全体へ貼り合わせられるか
細部を省いても、同じ問題を検出できるか
読み方を変えたときに診断が保たれるか
変更の順番や移行経路を変えても、整合するか
異なる経路で得た構造と操作が対応するか
要求を保つ変更には、どんな選択肢があるか
構造を保つ写像を分類できるか
担当ごとの記述から、全体の設計と変更を決められるか
局所データから対象と写像を再構成できるか
たとえば、データの形式を変えても、同じ操作ができるようにしたいとします。変換前後の対象をX,Y、変換を表す写像をh、それぞれで行う操作をT_X,T_Yとすると、その条件は次の等式で表せます。
h(T_X(x))=T_Y(h(x)).
操作してから変換しても、変換してから操作しても、結果が一致するという条件です。変換前後で値が対応するだけでなく、操作との関係も保たれるかを調べられます。
コードの細部を省いても、同じ判定ができる条件
対象から情報を取り出す方法を「読み」と呼びます。細部を省いて読んでも、Lawを満たすかが分かるなら、その判定には十分です。このように、細かな違いを区別せずにまとめることを粗視化といいます。
ただし、Lawを満たす対象と満たさない対象が同じ観測結果になってしまうなら、必要な情報まで省いています。
観測した情報だけでLawを評価できるか
対象をx、そこから情報を取り出す読みをq、Lawの評価をLとします。読み取った情報q(x)だけから評価する方法を\bar{L}とすると、必要なのは次の関係です。
L(x)=\bar{L}(q(x)).
読み取った情報だけで、対象全体を調べたときと同じ評価が得られる、という関係です。
たとえば、x=(u,v)からq(u,v)=u+vだけを読み取るとします。Lawがu+v=2なら、この観測値だけで判定できます。しかし、u=vかどうかは分かりません。(0,2)と(1,1)はどちらも観測値が2なのに、u=vを満たすのは後者だけだからです。
ソフトウェアでも、確かめたいLawによって、読む必要のある情報は変わります。「UI層から永続化層を直接呼ばない」なら、呼出し関係と各処理が属する層が分かれば判定できます。処理の中でどんな計算をしているかまで読む必要はありません。一方、返金額が支払額を超えないことは、その情報だけでは分かりません。Lawを先に決めることで、何を省いてよいかを判断できます。
読みの粒度と診断を結ぶAtlas定理
部分同士の食い違いには、各部分の値を調整すれば消せるものと、それでも残るものがあります。この違いを扱うのがコホモロジーです。調整しても残る食い違いを、障害類として捉えます。
三つの部分A、B、Cの間の差を考えます。AからB、BからC、CからAの向きに足すと、合計が1になるとします。
各部分の値を、それぞれu_A,u_B,u_Cだけ調整します。すると辺の差には、u_B-u_A、u_C-u_B、u_A-u_Cが加わります。しかし、これらの合計は0です。
(u_B-u_A)+(u_C-u_B)+(u_A-u_C)=0.
各部分の値を調整すると辺の差は変わりますが、一周したときの合計は変わりません。最初にあった差1は、許された調整では消せない食い違いとして残ります。
Atlas定理は、細かく読む場合と粗く読む場合で、この消せない食い違いを対応づけられる条件を示します。そのためには、どちらの読みでもLawを判定でき、部分の重なりや食い違いの計算方法も対応している必要があります。その条件を満たせば、細部を省いたせいで問題を見失ったり、余計な問題が生じたりすることなく診断できます。
たとえば、大きなコードベースを関数単位で調べる代わりに、モジュール単位にまとめて調べたいとします。このまとめ方がAtlasの条件を満たせば、そのLawについては、関数単位で調べたときと同じ食い違いを見つけられます。「全部読まないと不安だから読む」から、「この診断にはここまでの情報で足りる」へ、レビューの範囲を決める根拠が変わります。
部分ごとに直せても、全体で整合するとは限らない
大きな方程式系を部分に分けて解く場合、それぞれに解があっても、組み合わせられるとは限りません。共有する変数の値が一致する必要があるためです。
たとえば、一方の部分でu+v=2を解き、(u,v)=(0,2)を選んだとします。もう一方ではv+w=3を解き、(v,w)=(1,2)を選びます。どちらも自分の式を満たしますが、共有するvの値が違うため、そのまま一つの解にはできません。前者の解を保つなら、後者を(v,w)=(2,1)に選び直すことで、全体の解(u,v,w)=(0,2,1)が得られます。
各部分の解を、共有する部分で一致させ、一つの全体の解にすることを「貼り合わせ」と呼びます。AATでは層やコホモロジーを使って、この貼り合わせと、それを妨げる食い違いを調べます。
SAGA：方程式から、修復を妨げるものを見つける
方程式を解くときは変数の値を変えますが、ソフトウェアを直すときは、許された操作で設定や構造を変えます。計算結果を修復に使うには、どの操作がどの値の変更に当たるかを結び付ける必要があります。
SAGA比較定理は、修復の操作から作った障害と、方程式から作った障害を結び付けます。操作と方程式の対応が定理の条件を満たせば、修復を妨げるものがあるかどうかを、方程式の計算で調べられます。
たとえば、複数のサービスをそれぞれ修正できても、共有するデータや設定について修正内容が食い違えば、一緒には適用できません。各サービスで許す修正と、共有部分の条件を方程式に対応づけると、障害が残ることは「この操作の範囲では、各サービスの修正を両立できない」という意味になります。さらに貼り合わせの条件も満たせば、障害がゼロであることから、両立する全体の修復が存在すると言えます。
アリアドネ：変更を許した範囲で修復を求める
アリアドネでは、変更してよい部分と、そのままにしておく部分を決めます。その範囲で直せるかを調べ、直せる場合には修復の候補を求めます。
たとえば、二つの部分が同じ補正uを使い、一方ではu=x、他方ではu=yを要求するとします。x,yは目標として与えられた値です。
\begin{cases}
u=x,\
u=y.
\end{cases}
解があるのはx=yのときだけです。二つの式を引くと左辺は0になりますが、右辺にはy-xが残ります。この差が0でなければ、uをどう変えても修復できません。
二つ目の部分にだけ補正vを加えることを許すと、式は変わります。
\begin{cases}
u=x,\
u+v=y.
\end{cases}
今度はu=x、v=y-xとすれば解が得られます。変更できる範囲を広げたことで、以前は届かなかった目標を実現できます。
アリアドネは、有限・線形モデルで、各部分の条件から修復を求めます。修復できない場合には、その妨げとなるものを示します。
ソフトウェアの修正でも、「共有設定は変えず、このサービスの設定だけを変える」といった制約があります。設定値とLawをこのモデルで表せれば、修正案を何度も試す前に、その範囲で直せるかを調べられます。直せるなら候補の値を求め、直せないなら共有設定の変更も許すなど、範囲を広げて調べ直せます。
具体的な修復に必要な情報を観測する
補正vを加えた連立方程式には、どのx,yに対しても解があります。そのため、値を知らなくても「修復できる」と答えられます。しかし、具体的な補正値u,vを返すには、xとy-xを知る必要があります。
「解があるか」と「解を一つ返すか」では、必要な情報が違います。たとえばx,yを個別に読み取るなら、両方の値が必要です。既にxを知っていれば、追加で調べるのはyだけで済みます。
修復候補を決めるのに共有設定の値が足りないなら、AIにその設定を調べてもらう。修復の方程式は、次に何を観測するかを決める手がかりにもなります。
局所の記述から、全体の構造と変更を組み立てる
大きなソフトウェアを分担して調べたとき、各担当がまとめた情報から、全体の構造や変更を組み立てたいことがあります。
Rising Sea論文の局所再構成定理は、部分ごとの記述から全体を組み立てるための条件を示します。部品の情報だけを集めるのではなく、操作やLaw、共有部分での一致も含めて記述します。必要な条件を満たせば、全体の構造に加え、その構造を保つ変更も組み立てられます。
たとえば、複数のAIにモジュールごとの調査や変更案の作成を任せたとします。各AIの記述を定理が求める形に揃え、共有部分で食い違いがなく、操作も対応していることを確かめます。条件を満たせば、各担当の変更を一つの全体の変更に組み立てられます。個別にはよさそうな案が、全体でも両立するかを調べられるのです。
診断や修復、変更の比較、全体の再構成といった問題を、AtomとLawから作る共通の構造で扱えることが、AATの強みです。
形式検証や証明を使った開発とのつながり
守りたい性質を明示して確かめる考え方には、TLA+やAlloyなどの形式手法があります。TLA+はシステムの振る舞いを仕様として書き、モデル検査や証明で性質を確かめます。Alloyは関係や制約を記述し、それを満たす例や、性質を破る反例を探します。こうしたモデルを実装とは別に書く場合、コードの変更に合わせてモデルも更新し、両者の対応を保つ手間がかかります。
守りたいルールとその証明をコードと一緒に書く例が、Bend 2です。ルールをlawとして宣言し、それを満たす証明をコンパイラでチェックします。
ArchSigを通じてAATを使う強みは、ソースコードを実装についての唯一の真実として、後から診断を加えられることです。守りたい性質はLawに書き、実装の状態はその時点のコードから読み取ります。ArchMapは観測のたびに作り直せるので、コードと並行して手で更新し続ける必要がありません。
AIにはコードを書き進めてもらい、必要な時点で観測して診断します。実装のたびに別のモデルや証明を完成させる工程を挟まないため、AIがコードを書く速度を活かしながら変更を確かめられます。
自動判定の限界を示すのが、Riceの定理です。プログラムが計算する関数について、ある性質を考えます。それを満たすプログラムと満たさないプログラムがあるなら、どんなプログラムに対しても必ず停止して正しく判定するアルゴリズムは存在しません。だからこそ、どのLawを、どんなモデルで調べるかが大切です。有限のモデルや線形方程式で扱える範囲に絞れば、その範囲で判定や修復を計算できます。
コードを読む開発から、Lawをもとに観測する開発へ
今後ArchSigでは、変更してよい範囲を指定し、Lawを満たす修復の候補をモデル上で求められるようにしたいと考えています。候補がなければ、何が妨げているかを示します。候補を決めるための情報が足りなければ、AIが必要なコードや仕様を追加で読みます。その候補に沿ってコードを直し、もう一度観測して、テストでも確かめます。
候補が複数あれば、人が性能や保守性、移行の負担を見て選びます。
その出発点は、変更後も守りたい性質を書き出すことです。何を守るかをLawにし、必要な情報をAIに観測してもらい、数学で診断や修復を考える。コードをすべて読むことに頼らず、変更を判断する開発を目指しています。
リポジトリ: AlgebraicArchitectureTheoryV2
Bend: A Language That Prevents AI Mistakes
Bend is an open-source language that prevents AI mistakes through proof. It ensures your code complies with defined laws, making it a reliable choice for critical applications. With over 24.1K GitHub stars, it's gaining attention for its powerful verification capabilities. Perfect for developers seeking to eliminate bugs from their code.
#bendlang #opensource #programming #ai #languages
Follow for more AI, automation, and open-source tools you can actually use.
Link:
bendlang/bend
[ar] Bend: لغة تمنع أخطاء الذكاء الاصطناعي
Bend هي لغة مفتوحة المصدر تمنع أخطاء الذكاء الاصطناعي من خلال التحقق. تضمن توافق الكود الخاص بك مع القوانين المحددة، مما يجعلها خيارًا موثوقًا للتطبيقات الحساسة. مع أكثر من 24.1 ألف نجمة على GitHub، تحظى Bend باهتمام متزايد بفضل قدراتها القوية في التحقق. إنها مثالية للمطورين الذين يسعون إلى التخلص من الأخطاء في أكوادهم.
#bendlang #opensource #programming #ai #languages
تابعنا للمزيد من أدوات الذكاء الاصطناعي والأتمتة والمصادر المفتوحة التي يمكنك استخدامها فعليًا.
الرابط:
bendlang/bend
[bn] Bend: এমন একটি প্রোগ্রামিং ল্যাঙ্গুয়েজ যা এআই (AI)-এর ভুল রোধ করে
বেন্ড (Bend) একটি ওপেন-সোর্স ল্যাঙ্গুয়েজ যা প্রুফের মাধ্যমে এআই (AI) ভুল প্রতিরোধ করে। এটি নিশ্চিত করে যে আপনার কোড নির্দিষ্ট নিয়মকানুন মেনে চলে, যা এটিকে গুরুত্বপূর্ণ অ্যাপ্লিকেশনের জন্য একটি নির্ভরযোগ্য বিকল্প করে তোলে। ২৪.১ হাজারের বেশি গিটহাব স্টার (GitHub stars) সহ, এটি তার শক্তিশালী ভেরিফিকেশন ক্ষমতার জন্য মনোযোগ আকর্ষণ করছে। যেসব ডেভেলপার তাদের কোড থেকে বাগ দূর করতে চান, তাদের জন্য এটি আদর্শ।
#bendlang #opensource #programming #ai #languages
আরও এআই, অটোমেশন এবং ওপেন-সোর্স টুলের জন্য ফলো করুন যা আপনি সত্যিই ব্যবহার করতে পারবেন।
লিঙ্ক:
bendlang/bend
[de-DE] Bend: Eine Programmiersprache, die KI-Fehler verhindert
Bend ist eine Open-Source-Sprache, die KI-Fehler durch Beweise verhindert. Sie stellt sicher, dass Ihr Code definierten Regeln entspricht und ist daher eine zuverlässige Wahl für kritische Anwendungen. Mit über 24.100 GitHub-Sternen gewinnt sie aufgrund ihrer leistungsstarken Verifizierungsfunktionen zunehmend an Bedeutung. Ideal für Entwickler, die Fehler in ihrem Code beseitigen möchten.
#bendlang #opensource #programmierung #ai #sprachen
Folgen Sie uns für weitere KI-, Automatisierungs- und Open-Source-Tools, die Sie tatsächlich nutzen können.
Link:
bendlang/bend
[es-US] Bend: Un lenguaje que evita errores de la IA
Bend es un lenguaje de código abierto que previene errores de IA mediante verificación. Garantiza que tu código cumpla con las leyes definidas, lo que lo convierte en una opción confiable para aplicaciones críticas. Con más de 24.100 estrellas en GitHub, está ganando popularidad por sus potentes capacidades de verificación. Ideal para desarrolladores que buscan eliminar errores de su código.
#bendlang #códigoabierto #programación #ia #lenguajes
Síguenos para descubrir más herramientas de IA, automatización y código abierto que puedes usar.
Enlace: bendlang/bend
[fr-FR] Bend : un langage pour éviter les erreurs de l'IA
Bend est un langage open source qui prévient les erreurs d'IA grâce à la vérification. Il garantit la conformité de votre code aux règles établies, ce qui en fait un choix fiable pour les applications critiques. Avec plus de 24 100 étoiles sur GitHub, il se distingue par ses puissantes capacités de vérification. Idéal pour les développeurs souhaitant éliminer les bugs de leur code.
#bendlang #opensource #programming #ai #languages
Suivez-nous pour découvrir d'autres outils d'IA, d'automatisation et open source vraiment utiles.
Lien :
bendlang/bend
[hi] Bend: एक ऐसी प्रोग्रामिंग भाषा जो AI की गलतियों को रोकती है
बेंड एक ओपन-सोर्स भाषा है जो प्रमाणिकता के माध्यम से AI की गलतियों को रोकती है। यह सुनिश्चित करती है कि आपका कोड निर्धारित नियमों का पालन करता है, जिससे यह महत्वपूर्ण अनुप्रयोगों के लिए एक विश्वसनीय विकल्प बन जाता है। 24.1K से अधिक GitHub स्टार्स के साथ, यह अपनी शक्तिशाली सत्यापन क्षमताओं के लिए ध्यान आकर्षित कर रही है। अपने कोड से बग्स को दूर करने के इच्छुक डेवलपर्स के लिए बिल्कुल उपयुक्त।
#bendlang #opensource #programming #ai #languages
उपयोग में आने वाले और भी AI, स्वचालन और ओपन-सोर्स टूल्स के लिए हमें फॉलो करें।
लिंक:
bendlang/bend
[id] Bend: Bahasa Pemrograman untuk Mencegah Kesalahan AI
Bend adalah bahasa sumber terbuka yang mencegah kesalahan AI melalui pembuktian. Bahasa ini memastikan kode Anda mematuhi hukum yang telah ditentukan, menjadikannya pilihan yang andal untuk aplikasi kritis. Dengan lebih dari 24.100 bintang GitHub, bahasa ini menarik perhatian karena kemampuan verifikasinya yang kuat. Sempurna untuk pengembang yang ingin menghilangkan bug dari kode mereka.
#bendlang #opensource #programming #ai #languages
Ikuti untuk mendapatkan lebih banyak alat AI, otomatisasi, dan sumber terbuka yang benar-benar dapat Anda gunakan.
Tautan:
bendlang/bend
[it] Bend: il linguaggio che previene gli errori dell'IA
Bend è un linguaggio open-source che previene gli errori nell'IA tramite la verifica. Garantisce che il codice sia conforme alle leggi definite, rendendolo una scelta affidabile per applicazioni critiche. Con oltre 24.100 stelle su GitHub, sta guadagnando popolarità per le sue potenti funzionalità di verifica. Perfetto per gli sviluppatori che desiderano eliminare i bug dal proprio codice.
#bendlang #opensource #programming #ai #languages
Seguici per scoprire altri strumenti open-source, di automazione e di IA che puoi effettivamente utilizzare.
Link:
bendlang/bend
[iw] Bend: שפת תכנות שמונעת טעויות של בינה מלאכותית
Bend היא שפת קוד פתוח המונעת טעויות בבינה מלאכותית באמצעות הוכחה. היא מבטיחה שהקוד שלך עומד בחוקים מוגדרים, מה שהופך אותה לבחירה אמינה עבור יישומים קריטיים. עם למעלה מ-24.1 אלף כוכבי GitHub, היא זוכה לתשומת לב בזכות יכולות האימות החזקות שלה. מושלם עבור מפתחים המבקשים לחסל באגים מהקוד שלהם.
#bendlang #קודפתוח #תכנות #בינה מלאכותית #שפות
עקבו אחר כלי בינה מלאכותית, אוטומציה וקוד פתוח נוספים שתוכלו להשתמש בהם בפועל.
קישור:
bendlang/bend
[ja] Bend：AIのミスを防ぐプログラミング言語
Bendは、証明によってAIの誤りを防止するオープンソース言語です。定義された法則にコードが準拠していることを保証するため、重要なアプリケーションにも安心して使用できます。GitHubで24,100以上のスターを獲得し、その強力な検証機能で注目を集めています。コードのバグを排除したい開発者にとって最適な言語です。
#bendlang #opensource #programming #ai #languages
AI、自動化、そして実際に使えるオープンソースツールをもっと知りたい方は、ぜひフォローしてください。
リンク：
bendlang/bend
[ko] Bend: AI의 실수를 방지하는 프로그래밍 언어
Bend는 검증을 통해 AI 오류를 방지하는 오픈 소스 언어입니다. 코드가 정의된 규칙을 준수하도록 보장하여 중요한 애플리케이션에 신뢰할 수 있는 선택이 됩니다. 24,100개 이상의 GitHub 스타를 획득하며 강력한 검증 기능으로 주목받고 있습니다. 코드에서 버그를 제거하려는 개발자에게 이상적인 선택입니다.
#bendlang #opensource #programming #ai #languages
더 많은 AI, 자동화 및 실제로 사용할 수 있는 오픈 소스 도구를 보려면 팔로우하세요.
링크:
bendlang/bend
[ml] Bend: AI പിഴവുകൾ തടയുന്ന ഒരു പ്രോഗ്രാമിംഗ് ഭാഷ
പ്രൂഫ് വഴി AI തെറ്റുകൾ തടയുന്ന ഒരു ഓപ്പൺ സോഴ്സ് ഭാഷയാണ് ബെൻഡ്. ഇത് നിങ്ങളുടെ കോഡ് നിർവചിക്കപ്പെട്ട നിയമങ്ങൾ പാലിക്കുന്നുണ്ടെന്ന് ഉറപ്പാക്കുന്നു, ഇത് നിർണായക ആപ്ലിക്കേഷനുകൾക്ക് വിശ്വസനീയമായ ഒരു തിരഞ്ഞെടുപ്പാക്കി മാറ്റുന്നു. 24.1K-ലധികം GitHub സ്റ്റാറുകളുള്ള ഇത്, അതിന്റെ ശക്തമായ സ്ഥിരീകരണ കഴിവുകൾക്ക് ശ്രദ്ധ നേടുന്നു. അവരുടെ കോഡിൽ നിന്ന് ബഗുകൾ ഇല്ലാതാക്കാൻ ആഗ്രഹിക്കുന്ന ഡെവലപ്പർമാർക്ക് അനുയോജ്യമാണ്.
#bendlang #opensource #programming #ai #languages
നിങ്ങൾക്ക് യഥാർത്ഥത്തിൽ ഉപയോഗിക്കാൻ കഴിയുന്ന കൂടുതൽ AI, ഓട്ടോമേഷൻ, ഓപ്പൺ സോഴ്സ് ഉപകരണങ്ങൾക്കായി പിന്തുടരുക.
ലിങ്ക്:
bendlang/bend
[nl-NL] Bend: Een taal die AI-fouten voorkomt
Bend is een open-source programmeertaal die AI-fouten voorkomt door middel van bewijsvoering. Het zorgt ervoor dat je code voldoet aan gedefinieerde regels, waardoor het een betrouwbare keuze is voor kritieke toepassingen. Met meer dan 24.100 sterren op GitHub trekt het de aandacht vanwege zijn krachtige verificatiemogelijkheden. Perfect voor ontwikkelaars die bugs uit hun code willen elimineren.
#bendlang #opensource #programmeren #ai #talen
Volg ons voor meer AI, automatisering en open-source tools die je daadwerkelijk kunt gebruiken.
Link:
bendlang/bend
[pa] Bend: ਇੱਕ ਪ੍ਰੋਗਰਾਮਿੰਗ ਭਾਸ਼ਾ ਜੋ AI ਦੀਆਂ ਗਲਤੀਆਂ ਨੂੰ ਰੋਕਦੀ ਹੈ
ਬੈਂਡ ਇੱਕ ਓਪਨ-ਸੋਰਸ ਭਾਸ਼ਾ ਹੈ ਜੋ ਸਬੂਤ ਰਾਹੀਂ AI ਗਲਤੀਆਂ ਨੂੰ ਰੋਕਦੀ ਹੈ। ਇਹ ਯਕੀਨੀ ਬਣਾਉਂਦੀ ਹੈ ਕਿ ਤੁਹਾਡਾ ਕੋਡ ਪਰਿਭਾਸ਼ਿਤ ਕਾਨੂੰਨਾਂ ਦੀ ਪਾਲਣਾ ਕਰਦਾ ਹੈ, ਇਸਨੂੰ ਮਹੱਤਵਪੂਰਨ ਐਪਲੀਕੇਸ਼ਨਾਂ ਲਈ ਇੱਕ ਭਰੋਸੇਯੋਗ ਵਿਕਲਪ ਬਣਾਉਂਦਾ ਹੈ। 24.1K ਤੋਂ ਵੱਧ GitHub ਸਿਤਾਰਿਆਂ ਦੇ ਨਾਲ, ਇਹ ਆਪਣੀਆਂ ਸ਼ਕਤੀਸ਼ਾਲੀ ਤਸਦੀਕ ਸਮਰੱਥਾਵਾਂ ਲਈ ਧਿਆਨ ਖਿੱਚ ਰਿਹਾ ਹੈ। ਡਿਵੈਲਪਰਾਂ ਲਈ ਸੰਪੂਰਨ ਜੋ ਆਪਣੇ ਕੋਡ ਤੋਂ ਬੱਗ ਖਤਮ ਕਰਨਾ ਚਾਹੁੰਦੇ ਹਨ।
#bendlang #opensource #programming #ai #languages
ਹੋਰ AI, ਆਟੋਮੇਸ਼ਨ, ਅਤੇ ਓਪਨ-ਸੋਰਸ ਟੂਲਸ ਲਈ ਫਾਲੋ ਕਰੋ ਜੋ ਤੁਸੀਂ ਅਸਲ ਵਿੱਚ ਵਰਤ ਸਕਦੇ ਹੋ।
ਲਿੰਕ:
bendlang/bend
[pl] Bend: Język, który zapobiega błędom AI
Bend to język open source, który zapobiega błędom w sztucznej inteligencji poprzez dowodzenie. Zapewnia zgodność kodu z określonymi prawami, co czyni go niezawodnym wyborem dla aplikacji o krytycznym znaczeniu. Z ponad 24,1 tys. gwiazdek na GitHubie, zyskuje na popularności dzięki swoim zaawansowanym możliwościom weryfikacji. Idealny dla programistów, którzy chcą wyeliminować błędy ze swojego kodu.
#bendlang #opensource #programowanie #sztuczna inteligencja #języki
Obserwuj, aby dowiedzieć się więcej o sztucznej inteligencji, automatyzacji i narzędziach open source, z których możesz faktycznie skorzystać.
Link:
bendlang/bend
[pt-BR] Bend: Uma Linguagem que Previne Erros de IA
Bend é uma linguagem de código aberto que previne erros de IA por meio de provas. Ela garante que seu código esteja em conformidade com as leis definidas, tornando-a uma escolha confiável para aplicações críticas. Com mais de 24,1 mil estrelas no GitHub, está ganhando destaque por seus poderosos recursos de verificação. Perfeita para desenvolvedores que buscam eliminar bugs de seus códigos.
#bendlang #opensource #programming #ai #languages
Siga para mais ferramentas de IA, automação e código aberto que você pode realmente usar.
Link:
bendlang/bend
[ru] Bend: язык программирования, который предотвращает ошибки ИИ
Bend — это язык программирования с открытым исходным кодом, предотвращающий ошибки ИИ с помощью доказательств. Он гарантирует соответствие вашего кода заданным законам, что делает его надежным выбором для критически важных приложений. Имея более 24,1 тыс. звезд на GitHub, он привлекает внимание своими мощными возможностями верификации. Идеально подходит для разработчиков, стремящихся устранить ошибки в своем коде.
#bendlang #opensource #programming #ai #languages
Подписывайтесь, чтобы узнать больше об ИИ, автоматизации и инструментах с открытым исходным кодом, которые вы действительно можете использовать.
Ссылка:
bendlang/bend
[ta] Bend: AI செய்யும் பிழைகளைத் தடுக்கும் ஒரு நிரலாக்க மொழி
பெண்ட் (Bend) என்பது ஒரு திறந்த மூல மொழியாகும், இது சான்றளிப்பின் மூலம் செயற்கை நுண்ணறிவு (AI) தவறுகளைத் தடுக்கிறது. இது உங்கள் குறியீடு வரையறுக்கப்பட்ட விதிகளுக்கு இணங்குவதை உறுதிசெய்கிறது, இதனால் இது முக்கியமான பயன்பாடுகளுக்கு ஒரு நம்பகமான தேர்வாக அமைகிறது. 24.1 ஆயிரத்திற்கும் மேற்பட்ட கிட்ஹப் (GitHub) நட்சத்திரங்களுடன், இது அதன் சக்திவாய்ந்த சரிபார்ப்புத் திறன்களுக்காகக் கவனத்தை ஈர்த்து வருகிறது. தங்கள் குறியீட்டிலிருந்து பிழைகளை நீக்க விரும்பும் டெவலப்பர்களுக்கு இது மிகவும் பொருத்தமானது.
#bendlang #opensource #programming #ai #languages
நீங்கள் உண்மையில் பயன்படுத்தக்கூடிய மேலும் பல AI, ஆட்டோமேஷன் மற்றும் திறந்த மூலக் கருவிகளுக்குப் பின்தொடரவும்.
இணைப்பு:
bendlang/bend
[te] Bend: AI తప్పులను నివారించే ప్రోగ్రామింగ్ లాంగ్వేజ్
బెండ్ అనేది ఒక ఓపెన్-సోర్స్ భాష, ఇది రుజువుల ద్వారా AI పొరపాట్లను నివారిస్తుంది. ఇది మీ కోడ్ నిర్వచించిన నియమాలకు అనుగుణంగా ఉందని నిర్ధారిస్తుంది, అందువల్ల ఇది కీలకమైన అప్లికేషన్లకు నమ్మదగిన ఎంపిక. 24.1K కంటే ఎక్కువ గిట్హబ్ స్టార్స్తో, ఇది తన శక్తివంతమైన ధృవీకరణ సామర్థ్యాల కారణంగా దృష్టిని ఆకర్షిస్తోంది. తమ కోడ్ నుండి బగ్స్ను తొలగించాలనుకునే డెవలపర్లకు ఇది చాలా అనువైనది.
#bendlang #opensource #programming #ai #languages
మీరు నిజంగా ఉపయోగించగల మరిన్ని AI, ఆటోమేషన్ మరియు ఓపెన్-సోర్స్ టూల్స్ కోసం ఫాలో అవ్వండి.
లింక్: bendlang/bend
[uk] Bend: мова, що запобігає помилкам ШІ
Bend — це мова програмування з відкритим вихідним кодом, яка запобігає помилкам штучного інтелекту за допомогою доказів. Вона гарантує, що ваш код відповідає визначеним законам, що робить її надійним вибором для критично важливих програм. Маючи понад 24,1 тисячі зірок на GitHub, вона привертає увагу завдяки своїм потужним можливостям перевірки. Ідеально підходить для розробників, які прагнуть усунути помилки зі свого коду.
#bendlang #відкритийвихіднийкод #програмування #штучнийінтелект #мов
Підпишіться, щоб дізнатися більше про інструменти штучного інтелекту, автоматизації та відкритого вихідного коду, які ви можете використовувати.
Посилання:
bendlang/bend
4 likes · 87 views
Mentions
I'm fine with others but no type inference is weird, is it much harder than eval or it's just rarely undecidable? somebody send a PR: github.com/bendlang/bend/blob/main/bend2/bendtt.l…
@adfbng @VictorTaelin Proposal based on the syntax research: bend#1873
Bend: A fast language that blocks AI mistakes via proof
By requiring the LLM to prove your requirements true mathematcially. bendlang/bend
Code Review Starts with What Must Stay True Software development has long assumed that people will read and understand the code. We choose clear names and break up long functions so that the next person can follow our intent. But when AI produces code continuously, human reading speed becomes a bottleneck. Reviewing a change means looking beyond the diff: surrounding logic and existing requirements matter too. The amount we need to read keeps growing. We need a way to observe code. Start by deciding which properties a change must preserve, then extract the information needed to check them. The aim is to judge a change by what it preserves and what it alters, without requiring someone to read the entire implementation. Express the properties you care about as Laws A Law states a property we want software to satisfy: how it should behave, how it should be structured, or what should remain true after a change. Specifications describe behavior. Design rules constrain structure and dependencies. Compatibility requirements identify behavior that must survive a change. All express something we want to be true of the software. Laws generalize these different requirements so we can work with them in a common framework. Once the subject and conditions are clear, familiar requirements can be written as Laws. | Where the requirement comes from | Property to preserve | What to examine | | --- | --- | --- | | Functional specification | Create order lines in basket order | The code that creates order lines | | Design rule | The UI layer must not call the persistence layer directly | Calls and layer membership | | API compatibility policy | Preserve existing response fields after a change | Response definitions before and after the change | | Business rule | A refund must not exceed the amount paid | The relationship between payment and refund amounts | Define an Atom vocabulary for checking those Laws To check a Law, we need to decide what to look for in the code and how to record it. Atom definitions provide that vocabulary. Each fact we extract is recorded as an Atom using those definitions. For “the UI layer must not call the persistence layer directly,” we record who calls whom and which layer each belongs to. For order-line sequencing, we record the kind of operation and its processing order. The same code calls for different observations depending on the property we want to check. An ArchMap collects the facts extracted from the code in this vocabulary. | Element | Role | | --- | --- | | Law | States a property the subject must satisfy | | Atom definitions | Define the kinds of subjects and values we can record | | ArchMap | Records observed facts in that vocabulary, with references to the source | We ask AI to observe the code, then check whether the values in the ArchMap satisfy the Laws. The Law and Atom vocabulary is independent of any particular language or framework. If we define operations by their meaning, such as “create an order line” or “allocate stock,” we can use the same Laws for Python and Java implementations. AI reads each implementation and records what it finds in the shared vocabulary. It can also interpret what a piece of code does in business terms. It might follow a sequence of calls across several functions and record, “this is where stock is allocated.” Observations can include meaning that is difficult to capture from syntax and type information alone. A real example: fixing stock allocation changed the display order django-oscar, an e-commerce framework built with Python and Django, has a useful example of a stock-allocation change affecting the order in which purchased items appeared. When an order is placed, the application creates order lines from the basket and allocates stock. Originally, both operations ran in one loop. In pseudocode: for line in basket_lines: create_order_line(line) allocate_stock(line) A change introduced a consistent processing order for stock allocation. The aim was to acquire stock locks in the same order when multiple orders were placed concurrently. Basket lines were sorted by their stock records before entering the loop: for line in sort_by_stockrecord(basket_lines): create_order_line(line) allocate_stock(line) This aligned the stock-allocation order. It also changed the order in which order lines were created, because both operations were still in the same loop. Suppose a basket contains a notebook followed by a pen, but their stock records sort in the opposite order. The code now creates the pen's order line first. Since django-oscar retrieved order lines in primary-key order, the change affected how items appeared in order details, invoices, and emails. Write down the two Laws There are two properties to check: | Law | Property | | --- | --- | | L1 | Allocate stock in stock-record order | | L2 | Create order lines in basket order | L1 is what the change is meant to achieve. L2 is what it must preserve. Ask AI to extract the operations and their order To check these Laws, we need the kind of each operation and the order in which it runs. We define the following Atom fields: | Field | What to record | | --- | --- | | kind | Order-line creation or stock allocation | | sequence | Basket order or stock-record order | | loop | Which loop contains the operation | Recording loop also helps explain why the two operations were reordered together. I gave AI these definitions and Laws and asked it to read the code before and after the sorting change. The resulting ArchMap contained these observations: | Version | Operation | Order | Loop | | --- | --- | --- | --- | | Before the change | Create order line | Basket order | 1 | | Before the change | Allocate stock | Basket order | 1 | | After sorting | Create order line | Stock-record order | 1 | | After sorting | Allocate stock | Stock-record order | 1 | The ArchMap also records source locations, so a value can be checked against the code it came from. Check both Laws with ArchSig ArchSig is a tool under development that checks observed information against Laws. Passing the Atom definitions, Laws, and ArchMaps to v0.6.0 produced these results: | Version | L1: allocate in stock-record order | L2: create order lines in basket order | | --- | --- | --- | | Before the change | Not satisfied | Satisfied | | After sorting | Satisfied | Not satisfied | The stock-allocation order was fixed, but the order-line sequence changed with it. An effect that is easy to miss when reviewing only the intended fix becomes something we can explicitly check once the property is written as a Law. Split the loop to satisfy both Laws The observations show that both operations are in the same loop. That is why changing the stock-allocation order also changed order-line creation. Splitting the loop lets each operation use the order it needs: for line in basket_lines: create_order_line(line) for line in sort_by_stockrecord(basket_lines): allocate_stock(line) This is also how django-oscar was fixed. PR #4594 introduced the stock-ordering change; PR #4598 separated the loops. Observing the repaired code with the same fields gave: | Operation | Order | Loop | | --- | --- | --- | | Create order line | Basket order | 1 | | Allocate stock | Stock-record order | 2 | Checking this ArchMap showed that both L1 and L2 were satisfied. Stock allocation now followed the required order, while order lines still followed the basket. Treat specifications and conventions as properties to preserve This example brings together an internal requirement about stock processing and a user-visible requirement about display order. Software also has design rules, compatibility commitments, and business rules. Some live in specifications; others are conventions shared by the team. Thinking of all of them as properties to preserve lets us put them on the same list of things to check after a change. That is the value of generalizing them as Laws: we can consider what we want to fix alongside what we need to keep. For each requirement, ask what must be true, and of what. The information needed to check it becomes clearer. Laws turn specifications and conventions into questions we can investigate in the code. Treat Laws as equations and explore the solution space If a Law is not satisfied, what should change? Expressing Laws as equations lets us look for repairs among their solutions. Software that satisfies several Laws at once can be viewed as a solution to a large system of simultaneous equations. Let \(x\) be a tuple of variables, and express the Laws as: $$ f_1(x)=0,\quad f_2(x)=0,\quad\ldots,\quad f_m(x)=0. $$ The tuples satisfying every equation form a solution set: $$ \mathcal S={x\mid f_1(x)=\cdots=f_m(x)=0}. $$ Diagnosis asks whether the current values belong to \(\mathcal S\). If they do not, we can search within \(\mathcal S\) for a state to move to. The same Laws support both finding a problem and repairing it. Each equation narrows the choices Take two rational-valued variables, \(u\) and \(v\), and one equation: $$ u+v=2. $$ There are infinitely many solutions, including \((u,v)=(0,2),(1,1),(2,0)\). In general, a solution has the form \((t,2-t)\), with \(t\) free to vary. Now add \(u-v=0\): $$ \begin{cases} u+v=2,\ u-v=0. \end{cases} $$ Adding the equations gives \(2u=2\), so the solution is uniquely \((u,v)=(1,1)\). If we also require \(u=0\), no solution satisfies all three equations. View the solutions geometrically Treating the variables as coordinates gives the solutions a geometric shape. The equations \(u+v=2\) and \(u-v=0\) describe lines, and \((1,1)\) is their intersection. Each additional equation narrows the candidates to points satisfying all the conditions. Algebraic geometry develops this idea using polynomials and rings. Specifying the values, operations, and relations lets us study spaces of solutions and maps between them. Algebraic Architecture Theory (AAT) brings this approach to software structure. It constructs Law equations and solution spaces from data describing states and operations. Studying these spaces gives us a way to reason about diagnosis, change, and repair. ArchSig applies this theory to software analysis. The allowed changes determine where we can search A repair does not necessarily allow every variable to change. Let \(x_0\) be the current state, and let \(\mathcal A(x_0)\) contain the states reachable through permitted changes. A repair candidate must also satisfy the Laws, so it lies in: $$ \mathcal A(x_0)\cap\mathcal S. $$ If this intersection is empty, the permitted changes cannot produce a repair. Otherwise, its elements are candidate repaired states. The system above had the solution \((1,1)\). Starting from \((0,2)\), we cannot reach it if \(u\) must stay at zero and only \(v\) may change. If both can change, we can choose \((1,1)\). Whether a repair exists depends on what we are allowed to change, even when the Laws stay the same. Build one structure from Atoms and Laws AAT brings Atoms and Laws together with the available operations and the relationships between parts. Its distinguishing idea is to use this common structure for diagnosis, repair, and comparison of changes. The foundations are developed in Foundations of Algebraic Architecture Theory: A Rising Sea of Geometry, Transport, Comparison, and Reconstruction. Bring facts, operations, and conditions together AAT starts mathematically from Atoms. Giving relationships to Atoms that represent components and operations lets us treat a software structure as a mathematical object. Laws specify the equations that object must satisfy. We also include the allowed operations and the states they can produce. This lets us ask whether Laws still hold after an operation and what is preserved by a change. To study a large object in parts, we specify the parts and what they share. We include the data for each part and how discrepancies between parts are measured. The paper calls the resulting structure a full geometry. Use the same structure to ask different questions Several familiar software questions can then be studied within that structure: | Software question | Mathematical question | | --- | --- | | Can individually correct parts conflict when combined? | Can local states be glued into a global state? | | Can we omit detail and still detect the same problems? | Is diagnosis preserved when the reading changes? | | Do different orders of changes or migration paths remain consistent? | Do the structures and operations obtained along different paths correspond? | | What changes preserve the requirements? | Can we classify structure-preserving maps? | | Can descriptions from separate teams determine the overall design and its changes? | Can we reconstruct objects and maps from local data? | For example, suppose we want to change a data format while keeping the same operations available. Let \(X\) and \(Y\) be the objects before and after conversion, \(h\) the conversion map, and \(T_X,T_Y\) the respective operations. We can express the required relationship as: $$ h(T_X(x))=T_Y(h(x)). $$ Operating and then converting must give the same result as converting and then operating. We can check not just that values correspond, but that the conversion respects the operations on them. When can we omit detail without changing the diagnosis? Call a way of extracting information from an object a reading. A reading can omit detail and still be sufficient to evaluate a Law. Combining cases without retaining every distinction is called coarse-graining. But if an object satisfying the Law and one violating it produce the same observation, we have discarded information we needed. Can the observation alone determine whether the Law holds? Let \(x\) be an object, \(q\) a reading, and \(L\) the evaluation of a Law. If \(\bar{L}\) evaluates the Law using only the observed information \(q(x)\), we need: $$ L(x)=\bar{L}(q(x)). $$ The observed information must give the same evaluation as examining the whole object. Suppose \(x=(u,v)\) and we observe only \(q(u,v)=u+v\). That is enough to decide whether \(u+v=2\). It is not enough to decide whether \(u=v\): both \((0,2)\) and \((1,1)\) produce an observation of 2, but only the latter satisfies \(u=v\). The same principle applies to software. To check that the UI layer never directly calls the persistence layer, call relationships and layer membership are enough. We do not need to inspect every calculation inside those functions. But that information cannot tell us whether a refund exceeds the payment. Choosing the Law first helps us decide what we can leave out. The Atlas theorem connects observation detail to diagnosis Some discrepancies between parts can be removed by adjusting the values in each part. Others remain. Cohomology captures this distinction, with persistent discrepancies represented by obstruction classes. Consider discrepancies between three parts, A, B, and C. Suppose they sum to 1 when followed around the cycle from A to B, B to C, and C back to A. Adjust the values at the three parts by \(u_A,u_B,u_C\). The discrepancies on the edges change by \(u_B-u_A\), \(u_C-u_B\), and \(u_A-u_C\). But those adjustments sum to zero: $$ (u_B-u_A)+(u_C-u_B)+(u_A-u_C)=0. $$ Adjusting the individual values changes the discrepancies along the edges, but not their sum around the cycle. The original discrepancy of 1 remains: these adjustments cannot remove it. The Atlas theorem gives conditions under which these persistent discrepancies correspond between a detailed reading and a coarser one. Both readings must support evaluation of the Laws, and the overlaps between parts and the calculations of discrepancies must correspond as well. Under those conditions, omitting detail neither hides an obstruction nor creates an extra one. Suppose we want to examine a large codebase at module level rather than function level. If that grouping satisfies the Atlas conditions, it preserves the diagnosis of discrepancies for the Laws being studied. We gain a basis for deciding how much to inspect: this information is enough for this diagnosis. Local repairs do not automatically fit together When a large system of equations is split into parts, each part may have a solution without those solutions fitting together. Shared variables must agree. Suppose one part solves \(u+v=2\) and chooses \((u,v)=(0,2)\). Another solves \(v+w=3\) and chooses \((v,w)=(1,2)\). Both satisfy their own equations, but they disagree on \(v\), so they cannot form a single solution. Keeping the first solution, we can choose \((v,w)=(2,1)\) for the second and obtain the global solution \((u,v,w)=(0,2,1)\). Combining local solutions that agree on their shared parts is called gluing. AAT uses sheaves and cohomology to study gluing and the discrepancies that obstruct it. SAGA: use equations to find what prevents a repair Solving equations changes variable values. Repairing software changes settings or structures through permitted operations. To use a calculation for repair, we must connect those operations to changes in values. The SAGA comparison theorem connects obstructions constructed from repair operations with obstructions constructed from equations. When that correspondence meets the theorem's conditions, we can use the equations to determine whether an obstruction to repair remains. For example, several services might each admit a fix, yet disagree about shared data or configuration. Those fixes cannot all be applied together. Once the permitted repairs and shared conditions are represented by the corresponding equations, a nonzero obstruction means the repairs cannot be made compatible within those operations. With the additional gluing conditions in place, a zero obstruction means a compatible global repair exists. Ariadne: find a repair within the allowed scope Ariadne lets us specify what may change and what must stay fixed. It asks whether a repair is possible within that scope and finds candidates when it is. Suppose two parts share a correction \(u\). One requires \(u=x\), and the other requires \(u=y\), where \(x,y\) are given target values: $$ \begin{cases} u=x,\ u=y. \end{cases} $$ A solution exists only when \(x=y\). Subtracting the first equation from the second leaves zero on the left and \(y-x\) on the right. If that difference is nonzero, no choice of \(u\) can repair the system. Now allow an additional correction \(v\) in the second part: $$ \begin{cases} u=x,\ u+v=y. \end{cases} $$ We can choose \(u=x\) and \(v=y-x\). Broadening the allowed changes makes the target reachable. Ariadne works with finite linear models, constructing repairs from the conditions on each part. When repair is impossible, it identifies what prevents it. Software fixes often have constraints such as “leave the shared configuration unchanged; modify only this service's settings.” If the settings and Laws can be expressed in this model, we can determine whether that scope admits a repair before repeatedly trying patches. If it does, we can compute candidate values. If it does not, we can broaden the scope, perhaps allowing changes to shared configuration, and check again. Observe the information needed for a concrete repair The system with the additional correction \(v\) has a solution for every \(x,y\). We can therefore answer “a repair exists” without knowing their values. Returning actual values for \(u,v\), however, requires knowing \(x\) and \(y-x\). Deciding whether a solution exists and producing one require different information. If we read \(x\) and \(y\) separately, we need both values. If \(x\) is already known, only \(y\) remains to be observed. If choosing a repair requires a missing configuration value, we can ask AI to inspect that configuration. The repair equations can also guide what to observe next. Reconstruct the whole from local descriptions When work on a large codebase is divided among several people or agents, we may want to assemble an overall structure or change from their separate descriptions. The local reconstruction theorem in the Rising Sea paper gives conditions for doing this. Local descriptions include operations, Laws, and agreement on shared parts, alongside information about individual components. When the required conditions hold, we can reconstruct both the overall structure and changes that preserve it. Suppose several AI agents investigate different modules and propose changes. We put their descriptions into the form required by the theorem and check that shared parts agree and operations correspond. If the conditions hold, their local changes can be assembled into a global change. We can ask whether proposals that look reasonable individually actually fit together. This ability to address diagnosis, repair, comparison of changes, and reconstruction through a common structure built from Atoms and Laws is AAT's central strength. Connections to formal verification and development with proofs Making desired properties explicit and checking them is also central to formal methods such as TLA+ and Alloy. TLA+ describes system behavior in specifications whose properties can be checked through model checking and proof. Alloy describes relations and constraints, then searches for satisfying examples or counterexamples to properties. When these models are written separately from the implementation, keeping the two aligned as code changes takes work. Bend 2 takes an approach in which rules and their proofs are written alongside the code. Rules are declared as laws, and the compiler checks their proofs. A strength of applying AAT through ArchSig is that source code remains the single source of truth about the implementation, with diagnosis added afterward. Desired properties are written as Laws; the state of the implementation is observed from the current code. An ArchMap can be regenerated with each observation, so it need not be maintained by hand in parallel with the code. AI can keep writing code while we observe and diagnose it at the points we choose. Each implementation change need not wait for a separate model or proof to be completed. This lets us check changes while retaining the speed of AI-assisted development. Rice's theorem establishes a limit on automatic analysis. Consider a property of the function a program computes. If some programs satisfy it and others do not, no algorithm can always terminate and correctly decide that property for every program. That makes the choice of Laws and models important. Within a suitable finite model or a system of linear equations, we can compute diagnoses and repairs for that scope. From reading code to observing it through Laws The next step I want for ArchSig is to let users specify what may change, then find candidate repairs that satisfy the Laws within the model. If no candidate exists, the tool should identify what prevents one. If information is missing, AI can read the relevant code or specification. We can then apply a candidate to the code, observe it again, and test the result. Where several candidates exist, people can choose among them based on performance, maintainability, and the cost of migration. The starting point is to write down what must remain true after a change. Express it as Laws, ask AI to extract the information needed to check them, and use mathematics to reason about diagnosis and repair. That is the kind of development I want to make possible: judging changes without depending on someone reading every line. --- Repository: AlgebraicArchitectureTheoryV2
守りたい性質からはじめるコード観測 これまでのソフトウェア開発は、人がコードを読んで理解することを前提にしてきました。分かりやすい名前を付け、長い処理を分けるのも、読む人が意図を追えるようにするためです。 しかし、AIが次々にコードを書くようになると、人が読む速度では追いつきません。変更された箇所だけでなく、周囲の処理や既存の仕様まで確かめようとすれば、読む量はさらに増えます。 これからは、コードを観測するという考え方が必要です。まず、変更後も守りたい性質を決めます。そして、それが保たれているかを確かめるために、必要な情報をコードから取り出します。すべてを人が読み通さなくても、何を守り、何が変わったかをもとに判断できるようにしたいのです。 守りたい仕様や規約を、Lawとして書く Lawは、ソフトウェアに求める性質を表すものです。どのように動いてほしいか、どんな構造であってほしいか、変更しても何を保ちたいかを書きます。 仕様はソフトウェアの振る舞いを、設計規約は内部の構造や依存関係を定めます。互換性を守るには、変更前のどの振る舞いを残すかを決めます。いずれも「ソフトウェアにこうあってほしい」という要求です。Lawは、こうした仕様や規約を一般化し、同じ枠組みで扱うためのものです。 対象と条件をはっきりさせれば、身近な仕様や規約もLawとして書けます。 要求の出どころ 守りたい性質の例 確認する対象 機能仕様 注文行はカゴの行順に作る 注文行を作る処理 設計規約 UI層から永続化層を直接呼び出さない 層と呼出しの関係 APIの互換性方針 変更後も既存の応答項目を保つ 変更前後の応答定義 業務ルール 返金額は支払額を超えない 支払額と返金額の関係 Lawを確かめるための語彙を、Atomとして定義する Lawに書いた性質を確かめるには、コードの何を調べ、どんな値として記録するかを決める必要があります。そのための語彙を、Atomの定義として用意します。コードから読み取った一つひとつの事実は、この語彙を使ってAtomとして記録します。 たとえば「UI層から永続化層を直接呼び出さない」なら、誰が誰を呼び出し、それぞれがどの層に属するかを記録します。注文行の順序を確かめたいなら、操作の種類と処理順序を記録します。同じコードでも、確かめたい性質によって、調べる項目が変わります。 この語彙に沿ってコードから読み取った事実をまとめるのが、ArchMapです。 要素 役割 Law 対象が満たすべき性質を記述する Atomの定義 対象の種類や観測する値の語彙を定める ArchMap その語彙に沿って観測した事実を、ソースの根拠とともに記録する AIにコードを観測してもらい、ArchMapに記録された値がLawを満たすかを確かめます。 LawやAtomの語彙は、特定の言語やフレームワークに縛られません。「注文行を作る」「在庫を引き当てる」といった意味で定義すれば、PythonでもJavaでも、同じLawで確かめられます。AIがそれぞれの実装を読み、共通の語彙で記録するからです。 AIには、その処理が業務上何をしているかも読み取ってもらえます。たとえば、複数の関数に分かれた処理を追い、「ここで在庫を引き当てている」と記録します。構文や型の情報だけでは捉えにくい意味も、観測に含められます。 【具体例】在庫処理を直したら、商品の表示順が変わった PythonとDjangoで作られたEC基盤のdjango-oscarに、在庫処理の修正が注文の表示順に影響した事例があります。 注文を確定するときは、カゴの商品から注文行を作り、在庫を引き当てます。もともとは、一つのループで両方を処理していました。擬似コードにすると、こうなります。 for line in basket_lines: create_order_line(line) allocate_stock(line) ここに、在庫を処理する順序を揃える修正が入りました。同時に複数の注文が入っても、在庫のロックを同じ順序で取るためです。在庫情報を持つレコード（stockrecord）の順に並べ替えてから、ループを回します。 for line in sort_by_stockrecord(basket_lines): create_order_line(line) allocate_stock(line) これで在庫の処理順は揃います。ところが、同じループで作っている注文行まで並べ替わってしまいました。 たとえば、カゴに「ノート、ペン」の順で入れていても、stockrecordの順序が逆なら、注文行は「ペン、ノート」の順に作られます。django-oscarでは注文行を主キー順に取得していたため、注文詳細や請求書、メールの表示順まで変わってしまったのです。 守りたいことを二つのLawにする この修正で確認したいのは、次の二つです。 Law 守りたいこと L1 在庫はstockrecord順に引き当てる L2 注文行はカゴ順に作る L1は今回の修正で実現したいこと、L2はその修正でも変えたくないことです。 AIに処理の種類と順序を読み取ってもらう この二つのLawを確かめるために、処理の種類と順序を調べます。Atomの定義には、次の項目を用意します。 項目 読み取ること kind 注文行の作成か、在庫の引当か sequence カゴ順か、stockrecord順か loop どのループに入っているか loopも記録すると、二つの処理が一緒に並べ替わった理由を追いやすくなります。 AIにこの定義とLawを渡し、変更前と並べ替え後のコードを読んでもらいました。ArchMapにまとめた結果が、次の表です。 コード 処理 順序 ループ 変更前 注文行作成 カゴ順 1 変更前 在庫引当 カゴ順 1 並べ替え後 注文行作成 stockrecord順 1 並べ替え後 在庫引当 stockrecord順 1 ArchMapには元のコードの位置も記録するので、気になる値があれば該当箇所を確認できます。 ArchSigで二つのLawをチェックする 観測した情報がLawを満たすかをチェックするツールが、開発中のArchSigです。v0.6.0にAtomの定義、Law、ArchMapを渡すと、次の結果になりました。 コード L1：在庫引当はstockrecord順 L2：注文行作成はカゴ順 変更前 満たさない 満たす 並べ替え後 満たす 満たさない 在庫の処理順は直りましたが、注文行の順序は変わってしまいました。修正の目的だけを見ていると見落としやすい影響も、守りたい性質をLawに書いておけば確認できます。 ループを分けて、両方のLawを満たす 観測結果を見ると、二つの処理は同じループに入っています。在庫引当の順序を変えたとき、注文行の作成順序も一緒に変わったのは、このためです。それぞれを必要な順序で処理するには、ループを分けます。 for line in basket_lines: create_order_line(line) for line in sort_by_stockrecord(basket_lines): allocate_stock(line) django-oscarで実際に行われた修正も、この形でした。在庫の処理順を揃えた変更はPR #4594、ループを分けた修正はPR #4598に記録されています。 修正後のコードも、同じ項目で観測しました。 処理 順序 ループ 注文行作成 カゴ順 1 在庫引当 stockrecord順 2 このArchMapをチェックすると、L1もL2も満たす結果になりました。在庫の処理順を直しつつ、注文行の順序も保てています。 仕様も規約も、守りたい性質として扱う 今回、一緒に確かめたのは、在庫処理の都合と、利用者に見える表示順でした。開発では、このほかにも設計規約、APIの互換性、業務上のルールなどを守る必要があります。仕様書に書かれているものもあれば、チームの慣習として共有されているものもあります。 こうした要求を「守りたい性質」として捉えると、仕様書にあっても慣習であっても、変更後に確かめる条件として並べられます。今回直したいことと、引き続き守ることを一緒に扱えるのが、Lawとして一般化する意義です。 それぞれの要求について「何が、どうなっていればよいか」を書くと、確認に必要な情報も見えてきます。Lawは、仕様や規約を、コードから確かめられる問いにするための考え方です。 Lawを方程式として捉え、解の空間を考える Lawを満たしていなければ、どう変えればよいでしょうか。Lawを方程式で表すと、修復の候補をその解として探せます。複数のLawを同時に満たすソフトウェアは、大きな連立方程式の解として捉えられます。 変数の組をxとし、Lawを次の方程式で表します。 f_1(x)=0,\quad f_2(x)=0,\quad\ldots,\quad f_m(x)=0. それぞれの式を満たす値の組を集めると、解の集合が得られます。 \mathcal S={x\mid f_1(x)=\cdots=f_m(x)=0}. 現在の値が\mathcal Sに入っているかを確かめるのが診断です。入っていなければ、\mathcal Sの中から変更先を探します。同じLawが、問題の発見にも修復にも使えます。 方程式を加えると、選択肢が絞られる 有理数を値に取る二つの変数u,vについて、まず一つの方程式を考えます。 u+v=2. 解は(u,v)=(0,2),(1,1),(2,0)など、無数にあります。一般には(t,2-t)と書け、tを自由に選べます。 ここにu-v=0を加えると、連立方程式になります。 \begin{cases} u+v=2,\ u-v=0. \end{cases} 二つの式を足すと2u=2なので、解は(u,v)=(1,1)に決まります。さらにu=0を要求すると、すべてを満たす解はなくなります。 解の集合を、幾何として調べる 変数を座標とみなすと、方程式の解を図形として眺められます。u+v=2とu-v=0はそれぞれ直線の方程式で、両方を満たす点(1,1)はその交点です。式を加えるたびに、それらを同時に満たす点へと候補が絞られます。 代数幾何では、この考え方を多項式や環の言葉で扱います。どの値を使い、どの演算を認め、どの関係式を課すかを定めることで、解の空間と、その間の写像を調べられます。 この考え方をソフトウェアの構造に広げるのが、AAT（代数幾何的アーキテクチャ論）です。状態や操作を表すデータから、Lawの方程式と解の空間を作ります。その空間を調べることで、診断や変更、修復を考えます。ArchSigは、この理論をソフトウェアの分析に応用するツールです。 変更の制約は、解を探す範囲を定める 修復では、すべての変数を自由に変えられるとは限りません。現在の値をx_0とし、許された変更で移れる先を集めた集合を\mathcal A(x_0)とします。その中でLawも満たすものを探すので、求める候補は次の共通部分にあります。 \mathcal A(x_0)\cap\mathcal S. この共通部分が空なら、許された変更だけでは修復できません。空でなければ、その要素が修復後の候補になります。 先ほどの連立方程式の解は(1,1)でした。現在の値が(0,2)で、uを0に固定したままvだけ変えるなら、解には到達できません。両方の変更を許せば、(1,1)を選べます。Lawが同じでも、どこまで変更してよいかによって、直せるかどうかが変わります。 AtomとLawから、共通の構造を作る AATでは、AtomとLawをもとに、どんな操作ができるか、部分同士がどう関わるかを一つの構造にまとめます。診断や修復、変更の比較に、同じ構造を使うのが特徴です。この基礎をまとめたのが、論文Foundations of Algebraic Architecture Theory: A Rising Sea of Geometry, Transport, Comparison, and Reconstructionです。 事実、操作、条件を一つの対象にまとめる AATでは、Atomを数学の出発点に置きます。部品の存在や操作などを表すAtomに関係を与えると、ソフトウェアの構造を一つの数学的な対象として扱えます。その対象が満たすべき方程式をLawとして指定します。 さらに、どの操作を許し、それによってどんな状態へ移れるかも含めます。現在の状態だけでなく、操作した後もLawを満たすか、変更の前後で何が保たれるかを調べるためです。 大きな対象を分けて調べるなら、どこで分け、どこを共有するかも決めます。さらに、各部分のデータと、部分同士の食い違いをどう測るかを組み込みます。論文では、これらをまとめた構造を「完全幾何」と呼んでいます。 同じ構造から、複数の問題を考える ソフトウェアに関するさまざまな問いを、この構造の上で考えられます。 ソフトウェアについての問い 共通の構造の上で調べること 各部分は正しくても、組み合わせると矛盾しないか 局所の状態を全体へ貼り合わせられるか 細部を省いても、同じ問題を検出できるか 読み方を変えたときに診断が保たれるか 変更の順番や移行経路を変えても、整合するか 異なる経路で得た構造と操作が対応するか 要求を保つ変更には、どんな選択肢があるか 構造を保つ写像を分類できるか 担当ごとの記述から、全体の設計と変更を決められるか 局所データから対象と写像を再構成できるか たとえば、データの形式を変えても、同じ操作ができるようにしたいとします。変換前後の対象をX,Y、変換を表す写像をh、それぞれで行う操作をT_X,T_Yとすると、その条件は次の等式で表せます。 h(T_X(x))=T_Y(h(x)). 操作してから変換しても、変換してから操作しても、結果が一致するという条件です。変換前後で値が対応するだけでなく、操作との関係も保たれるかを調べられます。 コードの細部を省いても、同じ判定ができる条件 対象から情報を取り出す方法を「読み」と呼びます。細部を省いて読んでも、Lawを満たすかが分かるなら、その判定には十分です。このように、細かな違いを区別せずにまとめることを粗視化といいます。 ただし、Lawを満たす対象と満たさない対象が同じ観測結果になってしまうなら、必要な情報まで省いています。 観測した情報だけでLawを評価できるか 対象をx、そこから情報を取り出す読みをq、Lawの評価をLとします。読み取った情報q(x)だけから評価する方法を\bar{L}とすると、必要なのは次の関係です。 L(x)=\bar{L}(q(x)). 読み取った情報だけで、対象全体を調べたときと同じ評価が得られる、という関係です。 たとえば、x=(u,v)からq(u,v)=u+vだけを読み取るとします。Lawがu+v=2なら、この観測値だけで判定できます。しかし、u=vかどうかは分かりません。(0,2)と(1,1)はどちらも観測値が2なのに、u=vを満たすのは後者だけだからです。 ソフトウェアでも、確かめたいLawによって、読む必要のある情報は変わります。「UI層から永続化層を直接呼ばない」なら、呼出し関係と各処理が属する層が分かれば判定できます。処理の中でどんな計算をしているかまで読む必要はありません。一方、返金額が支払額を超えないことは、その情報だけでは分かりません。Lawを先に決めることで、何を省いてよいかを判断できます。 読みの粒度と診断を結ぶAtlas定理 部分同士の食い違いには、各部分の値を調整すれば消せるものと、それでも残るものがあります。この違いを扱うのがコホモロジーです。調整しても残る食い違いを、障害類として捉えます。 三つの部分A、B、Cの間の差を考えます。AからB、BからC、CからAの向きに足すと、合計が1になるとします。 各部分の値を、それぞれu_A,u_B,u_Cだけ調整します。すると辺の差には、u_B-u_A、u_C-u_B、u_A-u_Cが加わります。しかし、これらの合計は0です。 (u_B-u_A)+(u_C-u_B)+(u_A-u_C)=0. 各部分の値を調整すると辺の差は変わりますが、一周したときの合計は変わりません。最初にあった差1は、許された調整では消せない食い違いとして残ります。 Atlas定理は、細かく読む場合と粗く読む場合で、この消せない食い違いを対応づけられる条件を示します。そのためには、どちらの読みでもLawを判定でき、部分の重なりや食い違いの計算方法も対応している必要があります。その条件を満たせば、細部を省いたせいで問題を見失ったり、余計な問題が生じたりすることなく診断できます。 たとえば、大きなコードベースを関数単位で調べる代わりに、モジュール単位にまとめて調べたいとします。このまとめ方がAtlasの条件を満たせば、そのLawについては、関数単位で調べたときと同じ食い違いを見つけられます。「全部読まないと不安だから読む」から、「この診断にはここまでの情報で足りる」へ、レビューの範囲を決める根拠が変わります。 部分ごとに直せても、全体で整合するとは限らない 大きな方程式系を部分に分けて解く場合、それぞれに解があっても、組み合わせられるとは限りません。共有する変数の値が一致する必要があるためです。 たとえば、一方の部分でu+v=2を解き、(u,v)=(0,2)を選んだとします。もう一方ではv+w=3を解き、(v,w)=(1,2)を選びます。どちらも自分の式を満たしますが、共有するvの値が違うため、そのまま一つの解にはできません。前者の解を保つなら、後者を(v,w)=(2,1)に選び直すことで、全体の解(u,v,w)=(0,2,1)が得られます。 各部分の解を、共有する部分で一致させ、一つの全体の解にすることを「貼り合わせ」と呼びます。AATでは層やコホモロジーを使って、この貼り合わせと、それを妨げる食い違いを調べます。 SAGA：方程式から、修復を妨げるものを見つける 方程式を解くときは変数の値を変えますが、ソフトウェアを直すときは、許された操作で設定や構造を変えます。計算結果を修復に使うには、どの操作がどの値の変更に当たるかを結び付ける必要があります。 SAGA比較定理は、修復の操作から作った障害と、方程式から作った障害を結び付けます。操作と方程式の対応が定理の条件を満たせば、修復を妨げるものがあるかどうかを、方程式の計算で調べられます。 たとえば、複数のサービスをそれぞれ修正できても、共有するデータや設定について修正内容が食い違えば、一緒には適用できません。各サービスで許す修正と、共有部分の条件を方程式に対応づけると、障害が残ることは「この操作の範囲では、各サービスの修正を両立できない」という意味になります。さらに貼り合わせの条件も満たせば、障害がゼロであることから、両立する全体の修復が存在すると言えます。 アリアドネ：変更を許した範囲で修復を求める アリアドネでは、変更してよい部分と、そのままにしておく部分を決めます。その範囲で直せるかを調べ、直せる場合には修復の候補を求めます。 たとえば、二つの部分が同じ補正uを使い、一方ではu=x、他方ではu=yを要求するとします。x,yは目標として与えられた値です。 \begin{cases} u=x,\ u=y. \end{cases} 解があるのはx=yのときだけです。二つの式を引くと左辺は0になりますが、右辺にはy-xが残ります。この差が0でなければ、uをどう変えても修復できません。 二つ目の部分にだけ補正vを加えることを許すと、式は変わります。 \begin{cases} u=x,\ u+v=y. \end{cases} 今度はu=x、v=y-xとすれば解が得られます。変更できる範囲を広げたことで、以前は届かなかった目標を実現できます。 アリアドネは、有限・線形モデルで、各部分の条件から修復を求めます。修復できない場合には、その妨げとなるものを示します。 ソフトウェアの修正でも、「共有設定は変えず、このサービスの設定だけを変える」といった制約があります。設定値とLawをこのモデルで表せれば、修正案を何度も試す前に、その範囲で直せるかを調べられます。直せるなら候補の値を求め、直せないなら共有設定の変更も許すなど、範囲を広げて調べ直せます。 具体的な修復に必要な情報を観測する 補正vを加えた連立方程式には、どのx,yに対しても解があります。そのため、値を知らなくても「修復できる」と答えられます。しかし、具体的な補正値u,vを返すには、xとy-xを知る必要があります。 「解があるか」と「解を一つ返すか」では、必要な情報が違います。たとえばx,yを個別に読み取るなら、両方の値が必要です。既にxを知っていれば、追加で調べるのはyだけで済みます。 修復候補を決めるのに共有設定の値が足りないなら、AIにその設定を調べてもらう。修復の方程式は、次に何を観測するかを決める手がかりにもなります。 局所の記述から、全体の構造と変更を組み立てる 大きなソフトウェアを分担して調べたとき、各担当がまとめた情報から、全体の構造や変更を組み立てたいことがあります。 Rising Sea論文の局所再構成定理は、部分ごとの記述から全体を組み立てるための条件を示します。部品の情報だけを集めるのではなく、操作やLaw、共有部分での一致も含めて記述します。必要な条件を満たせば、全体の構造に加え、その構造を保つ変更も組み立てられます。 たとえば、複数のAIにモジュールごとの調査や変更案の作成を任せたとします。各AIの記述を定理が求める形に揃え、共有部分で食い違いがなく、操作も対応していることを確かめます。条件を満たせば、各担当の変更を一つの全体の変更に組み立てられます。個別にはよさそうな案が、全体でも両立するかを調べられるのです。 診断や修復、変更の比較、全体の再構成といった問題を、AtomとLawから作る共通の構造で扱えることが、AATの強みです。 形式検証や証明を使った開発とのつながり 守りたい性質を明示して確かめる考え方には、TLA+やAlloyなどの形式手法があります。TLA+はシステムの振る舞いを仕様として書き、モデル検査や証明で性質を確かめます。Alloyは関係や制約を記述し、それを満たす例や、性質を破る反例を探します。こうしたモデルを実装とは別に書く場合、コードの変更に合わせてモデルも更新し、両者の対応を保つ手間がかかります。 守りたいルールとその証明をコードと一緒に書く例が、Bend 2です。ルールをlawとして宣言し、それを満たす証明をコンパイラでチェックします。 ArchSigを通じてAATを使う強みは、ソースコードを実装についての唯一の真実として、後から診断を加えられることです。守りたい性質はLawに書き、実装の状態はその時点のコードから読み取ります。ArchMapは観測のたびに作り直せるので、コードと並行して手で更新し続ける必要がありません。 AIにはコードを書き進めてもらい、必要な時点で観測して診断します。実装のたびに別のモデルや証明を完成させる工程を挟まないため、AIがコードを書く速度を活かしながら変更を確かめられます。 自動判定の限界を示すのが、Riceの定理です。プログラムが計算する関数について、ある性質を考えます。それを満たすプログラムと満たさないプログラムがあるなら、どんなプログラムに対しても必ず停止して正しく判定するアルゴリズムは存在しません。だからこそ、どのLawを、どんなモデルで調べるかが大切です。有限のモデルや線形方程式で扱える範囲に絞れば、その範囲で判定や修復を計算できます。 コードを読む開発から、Lawをもとに観測する開発へ 今後ArchSigでは、変更してよい範囲を指定し、Lawを満たす修復の候補をモデル上で求められるようにしたいと考えています。候補がなければ、何が妨げているかを示します。候補を決めるための情報が足りなければ、AIが必要なコードや仕様を追加で読みます。その候補に沿ってコードを直し、もう一度観測して、テストでも確かめます。 候補が複数あれば、人が性能や保守性、移行の負担を見て選びます。 その出発点は、変更後も守りたい性質を書き出すことです。何を守るかをLawにし、必要な情報をAIに観測してもらい、数学で診断や修復を考える。コードをすべて読むことに頼らず、変更を判断する開発を目指しています。 リポジトリ: AlgebraicArchitectureTheoryV2
Bend: A Language That Prevents AI Mistakes Bend is an open-source language that prevents AI mistakes through proof. It ensures your code complies with defined laws, making it a reliable choice for critical applications. With over 24.1K GitHub stars, it's gaining attention for its powerful verification capabilities. Perfect for developers seeking to eliminate bugs from their code. #bendlang #opensource #programming #ai #languages Follow for more AI, automation, and open-source tools you can actually use. Link: bendlang/bend [ar] Bend: لغة تمنع أخطاء الذكاء الاصطناعي Bend هي لغة مفتوحة المصدر تمنع أخطاء الذكاء الاصطناعي من خلال التحقق. تضمن توافق الكود الخاص بك مع القوانين المحددة، مما يجعلها خيارًا موثوقًا للتطبيقات الحساسة. مع أكثر من 24.1 ألف نجمة على GitHub، تحظى Bend باهتمام متزايد بفضل قدراتها القوية في التحقق. إنها مثالية للمطورين الذين يسعون إلى التخلص من الأخطاء في أكوادهم. #bendlang #opensource #programming #ai #languages تابعنا للمزيد من أدوات الذكاء الاصطناعي والأتمتة والمصادر المفتوحة التي يمكنك استخدامها فعليًا. الرابط: bendlang/bend [bn] Bend: এমন একটি প্রোগ্রামিং ল্যাঙ্গুয়েজ যা এআই (AI)-এর ভুল রোধ করে বেন্ড (Bend) একটি ওপেন-সোর্স ল্যাঙ্গুয়েজ যা প্রুফের মাধ্যমে এআই (AI) ভুল প্রতিরোধ করে। এটি নিশ্চিত করে যে আপনার কোড নির্দিষ্ট নিয়মকানুন মেনে চলে, যা এটিকে গুরুত্বপূর্ণ অ্যাপ্লিকেশনের জন্য একটি নির্ভরযোগ্য বিকল্প করে তোলে। ২৪.১ হাজারের বেশি গিটহাব স্টার (GitHub stars) সহ, এটি তার শক্তিশালী ভেরিফিকেশন ক্ষমতার জন্য মনোযোগ আকর্ষণ করছে। যেসব ডেভেলপার তাদের কোড থেকে বাগ দূর করতে চান, তাদের জন্য এটি আদর্শ। #bendlang #opensource #programming #ai #languages আরও এআই, অটোমেশন এবং ওপেন-সোর্স টুলের জন্য ফলো করুন যা আপনি সত্যিই ব্যবহার করতে পারবেন। লিঙ্ক: bendlang/bend [de-DE] Bend: Eine Programmiersprache, die KI-Fehler verhindert Bend ist eine Open-Source-Sprache, die KI-Fehler durch Beweise verhindert. Sie stellt sicher, dass Ihr Code definierten Regeln entspricht und ist daher eine zuverlässige Wahl für kritische Anwendungen. Mit über 24.100 GitHub-Sternen gewinnt sie aufgrund ihrer leistungsstarken Verifizierungsfunktionen zunehmend an Bedeutung. Ideal für Entwickler, die Fehler in ihrem Code beseitigen möchten. #bendlang #opensource #programmierung #ai #sprachen Folgen Sie uns für weitere KI-, Automatisierungs- und Open-Source-Tools, die Sie tatsächlich nutzen können. Link: bendlang/bend [es-US] Bend: Un lenguaje que evita errores de la IA Bend es un lenguaje de código abierto que previene errores de IA mediante verificación. Garantiza que tu código cumpla con las leyes definidas, lo que lo convierte en una opción confiable para aplicaciones críticas. Con más de 24.100 estrellas en GitHub, está ganando popularidad por sus potentes capacidades de verificación. Ideal para desarrolladores que buscan eliminar errores de su código. #bendlang #códigoabierto #programación #ia #lenguajes Síguenos para descubrir más herramientas de IA, automatización y código abierto que puedes usar. Enlace: bendlang/bend [fr-FR] Bend : un langage pour éviter les erreurs de l'IA Bend est un langage open source qui prévient les erreurs d'IA grâce à la vérification. Il garantit la conformité de votre code aux règles établies, ce qui en fait un choix fiable pour les applications critiques. Avec plus de 24 100 étoiles sur GitHub, il se distingue par ses puissantes capacités de vérification. Idéal pour les développeurs souhaitant éliminer les bugs de leur code. #bendlang #opensource #programming #ai #languages Suivez-nous pour découvrir d'autres outils d'IA, d'automatisation et open source vraiment utiles. Lien : bendlang/bend [hi] Bend: एक ऐसी प्रोग्रामिंग भाषा जो AI की गलतियों को रोकती है बेंड एक ओपन-सोर्स भाषा है जो प्रमाणिकता के माध्यम से AI की गलतियों को रोकती है। यह सुनिश्चित करती है कि आपका कोड निर्धारित नियमों का पालन करता है, जिससे यह महत्वपूर्ण अनुप्रयोगों के लिए एक विश्वसनीय विकल्प बन जाता है। 24.1K से अधिक GitHub स्टार्स के साथ, यह अपनी शक्तिशाली सत्यापन क्षमताओं के लिए ध्यान आकर्षित कर रही है। अपने कोड से बग्स को दूर करने के इच्छुक डेवलपर्स के लिए बिल्कुल उपयुक्त। #bendlang #opensource #programming #ai #languages उपयोग में आने वाले और भी AI, स्वचालन और ओपन-सोर्स टूल्स के लिए हमें फॉलो करें। लिंक: bendlang/bend [id] Bend: Bahasa Pemrograman untuk Mencegah Kesalahan AI Bend adalah bahasa sumber terbuka yang mencegah kesalahan AI melalui pembuktian. Bahasa ini memastikan kode Anda mematuhi hukum yang telah ditentukan, menjadikannya pilihan yang andal untuk aplikasi kritis. Dengan lebih dari 24.100 bintang GitHub, bahasa ini menarik perhatian karena kemampuan verifikasinya yang kuat. Sempurna untuk pengembang yang ingin menghilangkan bug dari kode mereka. #bendlang #opensource #programming #ai #languages Ikuti untuk mendapatkan lebih banyak alat AI, otomatisasi, dan sumber terbuka yang benar-benar dapat Anda gunakan. Tautan: bendlang/bend [it] Bend: il linguaggio che previene gli errori dell'IA Bend è un linguaggio open-source che previene gli errori nell'IA tramite la verifica. Garantisce che il codice sia conforme alle leggi definite, rendendolo una scelta affidabile per applicazioni critiche. Con oltre 24.100 stelle su GitHub, sta guadagnando popolarità per le sue potenti funzionalità di verifica. Perfetto per gli sviluppatori che desiderano eliminare i bug dal proprio codice. #bendlang #opensource #programming #ai #languages Seguici per scoprire altri strumenti open-source, di automazione e di IA che puoi effettivamente utilizzare. Link: bendlang/bend [iw] Bend: שפת תכנות שמונעת טעויות של בינה מלאכותית Bend היא שפת קוד פתוח המונעת טעויות בבינה מלאכותית באמצעות הוכחה. היא מבטיחה שהקוד שלך עומד בחוקים מוגדרים, מה שהופך אותה לבחירה אמינה עבור יישומים קריטיים. עם למעלה מ-24.1 אלף כוכבי GitHub, היא זוכה לתשומת לב בזכות יכולות האימות החזקות שלה. מושלם עבור מפתחים המבקשים לחסל באגים מהקוד שלהם. #bendlang #קודפתוח #תכנות #בינה מלאכותית #שפות עקבו אחר כלי בינה מלאכותית, אוטומציה וקוד פתוח נוספים שתוכלו להשתמש בהם בפועל. קישור: bendlang/bend [ja] Bend：AIのミスを防ぐプログラミング言語 Bendは、証明によってAIの誤りを防止するオープンソース言語です。定義された法則にコードが準拠していることを保証するため、重要なアプリケーションにも安心して使用できます。GitHubで24,100以上のスターを獲得し、その強力な検証機能で注目を集めています。コードのバグを排除したい開発者にとって最適な言語です。 #bendlang #opensource #programming #ai #languages AI、自動化、そして実際に使えるオープンソースツールをもっと知りたい方は、ぜひフォローしてください。 リンク： bendlang/bend [ko] Bend: AI의 실수를 방지하는 프로그래밍 언어 Bend는 검증을 통해 AI 오류를 방지하는 오픈 소스 언어입니다. 코드가 정의된 규칙을 준수하도록 보장하여 중요한 애플리케이션에 신뢰할 수 있는 선택이 됩니다. 24,100개 이상의 GitHub 스타를 획득하며 강력한 검증 기능으로 주목받고 있습니다. 코드에서 버그를 제거하려는 개발자에게 이상적인 선택입니다. #bendlang #opensource #programming #ai #languages 더 많은 AI, 자동화 및 실제로 사용할 수 있는 오픈 소스 도구를 보려면 팔로우하세요. 링크: bendlang/bend [ml] Bend: AI പിഴവുകൾ തടയുന്ന ഒരു പ്രോഗ്രാമിംഗ് ഭാഷ പ്രൂഫ് വഴി AI തെറ്റുകൾ തടയുന്ന ഒരു ഓപ്പൺ സോഴ്സ് ഭാഷയാണ് ബെൻഡ്. ഇത് നിങ്ങളുടെ കോഡ് നിർവചിക്കപ്പെട്ട നിയമങ്ങൾ പാലിക്കുന്നുണ്ടെന്ന് ഉറപ്പാക്കുന്നു, ഇത് നിർണായക ആപ്ലിക്കേഷനുകൾക്ക് വിശ്വസനീയമായ ഒരു തിരഞ്ഞെടുപ്പാക്കി മാറ്റുന്നു. 24.1K-ലധികം GitHub സ്റ്റാറുകളുള്ള ഇത്, അതിന്റെ ശക്തമായ സ്ഥിരീകരണ കഴിവുകൾക്ക് ശ്രദ്ധ നേടുന്നു. അവരുടെ കോഡിൽ നിന്ന് ബഗുകൾ ഇല്ലാതാക്കാൻ ആഗ്രഹിക്കുന്ന ഡെവലപ്പർമാർക്ക് അനുയോജ്യമാണ്. #bendlang #opensource #programming #ai #languages നിങ്ങൾക്ക് യഥാർത്ഥത്തിൽ ഉപയോഗിക്കാൻ കഴിയുന്ന കൂടുതൽ AI, ഓട്ടോമേഷൻ, ഓപ്പൺ സോഴ്സ് ഉപകരണങ്ങൾക്കായി പിന്തുടരുക. ലിങ്ക്: bendlang/bend [nl-NL] Bend: Een taal die AI-fouten voorkomt Bend is een open-source programmeertaal die AI-fouten voorkomt door middel van bewijsvoering. Het zorgt ervoor dat je code voldoet aan gedefinieerde regels, waardoor het een betrouwbare keuze is voor kritieke toepassingen. Met meer dan 24.100 sterren op GitHub trekt het de aandacht vanwege zijn krachtige verificatiemogelijkheden. Perfect voor ontwikkelaars die bugs uit hun code willen elimineren. #bendlang #opensource #programmeren #ai #talen Volg ons voor meer AI, automatisering en open-source tools die je daadwerkelijk kunt gebruiken. Link: bendlang/bend [pa] Bend: ਇੱਕ ਪ੍ਰੋਗਰਾਮਿੰਗ ਭਾਸ਼ਾ ਜੋ AI ਦੀਆਂ ਗਲਤੀਆਂ ਨੂੰ ਰੋਕਦੀ ਹੈ ਬੈਂਡ ਇੱਕ ਓਪਨ-ਸੋਰਸ ਭਾਸ਼ਾ ਹੈ ਜੋ ਸਬੂਤ ਰਾਹੀਂ AI ਗਲਤੀਆਂ ਨੂੰ ਰੋਕਦੀ ਹੈ। ਇਹ ਯਕੀਨੀ ਬਣਾਉਂਦੀ ਹੈ ਕਿ ਤੁਹਾਡਾ ਕੋਡ ਪਰਿਭਾਸ਼ਿਤ ਕਾਨੂੰਨਾਂ ਦੀ ਪਾਲਣਾ ਕਰਦਾ ਹੈ, ਇਸਨੂੰ ਮਹੱਤਵਪੂਰਨ ਐਪਲੀਕੇਸ਼ਨਾਂ ਲਈ ਇੱਕ ਭਰੋਸੇਯੋਗ ਵਿਕਲਪ ਬਣਾਉਂਦਾ ਹੈ। 24.1K ਤੋਂ ਵੱਧ GitHub ਸਿਤਾਰਿਆਂ ਦੇ ਨਾਲ, ਇਹ ਆਪਣੀਆਂ ਸ਼ਕਤੀਸ਼ਾਲੀ ਤਸਦੀਕ ਸਮਰੱਥਾਵਾਂ ਲਈ ਧਿਆਨ ਖਿੱਚ ਰਿਹਾ ਹੈ। ਡਿਵੈਲਪਰਾਂ ਲਈ ਸੰਪੂਰਨ ਜੋ ਆਪਣੇ ਕੋਡ ਤੋਂ ਬੱਗ ਖਤਮ ਕਰਨਾ ਚਾਹੁੰਦੇ ਹਨ। #bendlang #opensource #programming #ai #languages ਹੋਰ AI, ਆਟੋਮੇਸ਼ਨ, ਅਤੇ ਓਪਨ-ਸੋਰਸ ਟੂਲਸ ਲਈ ਫਾਲੋ ਕਰੋ ਜੋ ਤੁਸੀਂ ਅਸਲ ਵਿੱਚ ਵਰਤ ਸਕਦੇ ਹੋ। ਲਿੰਕ: bendlang/bend [pl] Bend: Język, który zapobiega błędom AI Bend to język open source, który zapobiega błędom w sztucznej inteligencji poprzez dowodzenie. Zapewnia zgodność kodu z określonymi prawami, co czyni go niezawodnym wyborem dla aplikacji o krytycznym znaczeniu. Z ponad 24,1 tys. gwiazdek na GitHubie, zyskuje na popularności dzięki swoim zaawansowanym możliwościom weryfikacji. Idealny dla programistów, którzy chcą wyeliminować błędy ze swojego kodu. #bendlang #opensource #programowanie #sztuczna inteligencja #języki Obserwuj, aby dowiedzieć się więcej o sztucznej inteligencji, automatyzacji i narzędziach open source, z których możesz faktycznie skorzystać. Link: bendlang/bend [pt-BR] Bend: Uma Linguagem que Previne Erros de IA Bend é uma linguagem de código aberto que previne erros de IA por meio de provas. Ela garante que seu código esteja em conformidade com as leis definidas, tornando-a uma escolha confiável para aplicações críticas. Com mais de 24,1 mil estrelas no GitHub, está ganhando destaque por seus poderosos recursos de verificação. Perfeita para desenvolvedores que buscam eliminar bugs de seus códigos. #bendlang #opensource #programming #ai #languages Siga para mais ferramentas de IA, automação e código aberto que você pode realmente usar. Link: bendlang/bend [ru] Bend: язык программирования, который предотвращает ошибки ИИ Bend — это язык программирования с открытым исходным кодом, предотвращающий ошибки ИИ с помощью доказательств. Он гарантирует соответствие вашего кода заданным законам, что делает его надежным выбором для критически важных приложений. Имея более 24,1 тыс. звезд на GitHub, он привлекает внимание своими мощными возможностями верификации. Идеально подходит для разработчиков, стремящихся устранить ошибки в своем коде. #bendlang #opensource #programming #ai #languages Подписывайтесь, чтобы узнать больше об ИИ, автоматизации и инструментах с открытым исходным кодом, которые вы действительно можете использовать. Ссылка: bendlang/bend [ta] Bend: AI செய்யும் பிழைகளைத் தடுக்கும் ஒரு நிரலாக்க மொழி பெண்ட் (Bend) என்பது ஒரு திறந்த மூல மொழியாகும், இது சான்றளிப்பின் மூலம் செயற்கை நுண்ணறிவு (AI) தவறுகளைத் தடுக்கிறது. இது உங்கள் குறியீடு வரையறுக்கப்பட்ட விதிகளுக்கு இணங்குவதை உறுதிசெய்கிறது, இதனால் இது முக்கியமான பயன்பாடுகளுக்கு ஒரு நம்பகமான தேர்வாக அமைகிறது. 24.1 ஆயிரத்திற்கும் மேற்பட்ட கிட்ஹப் (GitHub) நட்சத்திரங்களுடன், இது அதன் சக்திவாய்ந்த சரிபார்ப்புத் திறன்களுக்காகக் கவனத்தை ஈர்த்து வருகிறது. தங்கள் குறியீட்டிலிருந்து பிழைகளை நீக்க விரும்பும் டெவலப்பர்களுக்கு இது மிகவும் பொருத்தமானது. #bendlang #opensource #programming #ai #languages நீங்கள் உண்மையில் பயன்படுத்தக்கூடிய மேலும் பல AI, ஆட்டோமேஷன் மற்றும் திறந்த மூலக் கருவிகளுக்குப் பின்தொடரவும். இணைப்பு: bendlang/bend [te] Bend: AI తప్పులను నివారించే ప్రోగ్రామింగ్ లాంగ్వేజ్ బెండ్ అనేది ఒక ఓపెన్-సోర్స్ భాష, ఇది రుజువుల ద్వారా AI పొరపాట్లను నివారిస్తుంది. ఇది మీ కోడ్ నిర్వచించిన నియమాలకు అనుగుణంగా ఉందని నిర్ధారిస్తుంది, అందువల్ల ఇది కీలకమైన అప్లికేషన్లకు నమ్మదగిన ఎంపిక. 24.1K కంటే ఎక్కువ గిట్హబ్ స్టార్స్తో, ఇది తన శక్తివంతమైన ధృవీకరణ సామర్థ్యాల కారణంగా దృష్టిని ఆకర్షిస్తోంది. తమ కోడ్ నుండి బగ్స్ను తొలగించాలనుకునే డెవలపర్లకు ఇది చాలా అనువైనది. #bendlang #opensource #programming #ai #languages మీరు నిజంగా ఉపయోగించగల మరిన్ని AI, ఆటోమేషన్ మరియు ఓపెన్-సోర్స్ టూల్స్ కోసం ఫాలో అవ్వండి. లింక్: bendlang/bend [uk] Bend: мова, що запобігає помилкам ШІ Bend — це мова програмування з відкритим вихідним кодом, яка запобігає помилкам штучного інтелекту за допомогою доказів. Вона гарантує, що ваш код відповідає визначеним законам, що робить її надійним вибором для критично важливих програм. Маючи понад 24,1 тисячі зірок на GitHub, вона привертає увагу завдяки своїм потужним можливостям перевірки. Ідеально підходить для розробників, які прагнуть усунути помилки зі свого коду. #bendlang #відкритийвихіднийкод #програмування #штучнийінтелект #мов Підпишіться, щоб дізнатися більше про інструменти штучного інтелекту, автоматизації та відкритого вихідного коду, які ви можете використовувати. Посилання: bendlang/bend
For the first thing you're talking about check out bend. bendlang/bend
PC for software development/light gaming, at under £1000 My laptop recently died. My school provides laptops we can borrow, but they're quite limited in power/compute capability. I'm looking to build a setup which I can use comfortably at home/use remote desktop to access from school. I was mostly happy with the specs of my old laptop (i7 13th gen, 4050 laptop GPU, 16GB ddr5), so I'm looking to get a desktop of similar capacity. However, I did find myself having to close tabs because of RAM issues, so 32 GB would be nice. - New build or upgrade? - New build - Existing parts/monitors to reuse? - I have some shitty monitors which will make do/I can present the pc and the monitors (which should be fairly cheap anyways, as I don't need fps monitors) as separate items to my parents :p - PC purpose? - Mostly software development/related. - It needs a decent amoutn of RAM (I dug out an old laptop with 8GB RAM + 17GB swap and I'm still running out of memory and swap sometimes; I think resharper is the likely culprit but not much I can do about that) - Resharper is also heavy on CPU usage + competitions such as [ritangle](Ritangle - An MEI Competition for A level Students) mean a good CPU would be nice - I'm interested in GCGPU technologies, in particular stuff like [Bend](GitHub - HigherOrderCO/Bend1: Bend 1: the original massively parallel, high-level programming language (superseded by github.com/bendlang/bend) · GitHub) - Fucking around with SRS Scheduling, which currently involves playing with decently sized NNs - I also occasionally PC game in the form of heavily modded minecraft. Packs I've played before/are considering playing are: - gregtech - atm10 - create:mekanized - Purchase country? - UK - Monitors needed? - N/A, I think. If the hardware will limit number of monitors, I'd like at least two, and three would be nice) - Budget range? - £1000 maximum, but ideally more along the 500-800 range. I got my laptop for £500 a few years ago, so with the recent price increases a few hundred more is probably what my parents are/I am expecting - WiFi or wired connection? - I'd like WIFI, but we do have one of those wifi extender things which purports to allow running an ethernet cable out - Size/noise constraints? - It will be in my bedroom, so not too insane, but if louder/bigger means cheaper, that's fine by me - Color/lighting preferences? - None - Any other specific needs? As mentioned: - 32 GB RAM ideally - Nvidia GPU
Thanks @Lorenzoowb for the quick reviews and for showing me where the second fix really belonged. PRs if anyone's curious: bend#1398 bend#1428