Can we afford cheap code?

Adam Chlipala, a respected figure in formal verification, writes:

Code as we know it will become a throw-away automatic byproduct of the real long-lived artifacts, joining formats like assembly language that we mostly think of in that way today.

… economic forces will push toward simplifying the world in pockets of activity given over to automation – and over time, the fraction of the economy covered by such pockets will grow, and pockets will merge with each other.

Adam explores the ideas of spec-driven development and throwaway, transient code in a series of posts, including: Abstraction boundaries and bubbles of legibility, Rewrite All the Code, All the Time, Programming should be more like SQL. Generating code from specification will reduce implementation costs so drastically that everyone will line up to switch to engineering specifications instead of code.

But software engineering is more than writing code. The system and its environment are changing: its clients become reliant on undocumented behavior, its performance may strongly depend on a particular platform and workload, its state may have to survive an upgrade while requests keep arriving. Our understanding is catching up: we discover requirements, check and readjust assumptions, investigate failures.

Code generation guarantees that the implementation is correct, that it fits specification. Correct implementation is hard, but not always the hardest part of engineering. How will the economy of engineering change if we try to reorganize it around specification engineering and automatic code generation? How does it affect the costs of requirement discovery, debugging, validation, deployment? Does code generation make it easier to achieve nonfunctional properties, like low latency?

These costs deserve a larger place in the forecast. Automatic regeneration can be attractive where requirements are well understood and environmental assumptions are stable. For those curious about the other cases, I present my inquiry.

Non-functional properties

Adam writes:

Instead of storing conventional code in repositories, we would prefer to store the highest-level description of requirements that we can get away with, where available tools reliably automate the rest of bringing the desired program to life. Some nonfunctional requirements may change, in which case we can relatively simply fold them into the requirements and redo generation.

Nonfunctional properties and requirements often relate several systems. There are three main systems involved in engineering process:

Target system
the code during execution and its immediate runtime machinery.
Development system
software engineers, organizations, generators, tools, practices, and so on.
Operational milieu
hardware, adjacent services, users, institutions, physical processes, adversaries, regulators with which the target system interacts1, and so on.

Most if not all nonfunctional requirements relate some of these systems, or their subsystems. Performance concerns implementation, platform, workload. Reliability concerns implementation, deployment conditions, failure processes. Maintainability and diagnosability concern target and development systems. Usability relates target system and users, and so on. Sometimes we decompose systems further – in embedded software, timing, energy consumption, and reliability may depend on processor revision, caches and pipelines, interrupt behavior, temperature, voltage, sensor noise and calibration, mechanical wear…

Performance properties belong with nonfunctional bunch, and Adam suggests we'd have more static guarantees about it:

Another great example is performance, where I’m actually pretty surprised at how rare it has been for practical programming languages to support annotations that spell out performance requirements, so that it’s a compile-time error if code can’t be produced that is fast-enough, uses little-enough memory, etc.

First, I investigate why there are no worst-case resource requirements annotations2 in most programming languages. The argumentation survives when we pass from code to specification.

Code is not a system – it does not answers requests under 10 ms by itself. Latency is a property of specific hardware running this code in a specific environment under a specific workload. These may be unknown at compile-time. Performance requirements bind them together, so to express them in the specification (or code) we need models of the intended platform and workload3.

Performance requirements may also sit at different levels. Resource Aware ML, for example, can bound the number of abstract "steps" required to run a function over a list. It is then guaranteed that the function will take no more than 732 + 12 * M abstract steps, where M stands for the length of the list. This is a bound on an abstract resource, in a simplified model, not a bound on the running time of compiled code on a real platform, with real workload. In the end, we want guarantees on the latter.

But real systems are unbearably complex in essential ways, and so is deriving guaranteed properties for them. They often trade performance in rare worst cases for a better average, and resist worst case analysis.

  • Statically, they use aggressive compiler optimizations – hoisting, inlining, specialization, precomputations – which may degrade cold paths or trade resources e.g. allocate more memory but execute fewer instructions.
  • Dynamically, platforms implement out-of-order and speculative execution, multi-level cache hierarchies, NUMA interconnects, SSD controller garbage collection, and so on. On our desktop computers, hardware optimizations alone account for a difference of more than 6 orders of magnitude between best-case and worst-case memory access.
  • JIT compilation, if present, adds sauce in the sandwich.

Additionally, in embedded systems, real devices often contain silicon errata and board-specific workarounds that may never reach the manufacturer’s published model. How do we model them reliably?

We deal with intractable complex models by engineering pockets designed for predictability (I adopt Adam's pocket metaphor in this essay). We fix the hardware, simplify the context, close on the workload. Hardware should conform to a simple enough, known model.

Designing and maintaining a pocket may get expensive. First, it bumps complexity. A pocket with useful bounds on memory access imposes possibly unnatural restrictions on the underlying platform such as:

  • No swapping
  • Memory prefaulted
  • Fixed CPU affinity
  • Bounded interrupt behavior
  • Known cache hierarchy
  • Known TLB behavior
  • Bounded DRAM contention
  • Possibly isolated cores
  • Possibly disabled frequency scaling
  • No uncontrolled direct memory access

Predictability of the worst case taxes performance. We prefer a reliably slow, steady snail to a quick jumping frog.

Closing on workload means we need to either control the clients, or separate them behind a filtering layer. This works in selected domains, like avionics.

Another tax is paid in two kinds of validation required to support performance annotations and making them into real guarantees. First, easier kind: are costs accurate within the model? Second, harder: models decay, do ours still fit to the world? Workload changes, clients are updated independently, faulty CPU starts to lag on the same workload.

Keeping models adequate is complex and may require human oversight. Telemetry and AI help automating it, but I do not believe in zero oversight. The system can monitor that queue depth remains under a threshold, but it cannot infer that the threshold ceased to predict latency because a firmware update changed cache behavior. Humans still reason on a meta-level, revise models, choose among several possible repairs, notice that a new missed constraint is not expressible in current model, identify and resolve ethical and business-related questions.

To sum up, I believe, to enforce performance requirements statically in a real complex system, there are two extreme ways and a spectrum in between:

  1. Pay a premium in performance and effort for a predictable pocket, relocating complexity at its boundary. Inside the pocket, an adequate cost model can be simpler, workload is controllable, world is closed. We still need to reliably relate abstract costs to real measurable properties.
  2. Model the whole system (of which performance properties are emergent). Now we have a bundle of code, platform and workload models, and commitments to keep models adequate.

This picture remains once we move from engineering code to spec-driven code generation.

The same reasoning applies to other non functional requirements. At extremes, for a requirement that relates several systems, we either need to put them fully under our control and simplify them, making a pocket, or we put more models into the bundle, and commit to validating their adequacy.

Adam seems optimistic about nonfunctional requirements:

Some nonfunctional requirements may change, in which case we can relatively simply fold them into the requirements and redo generation.

I think "relatively simply" here can often unfold as "as simple as modeling relevant systems and continuously validating their adequacy". It is non-trivial to identify case when benefits outweigh these costs.

Ambition in abstraction

Adam compares writing specifications to writing high-level code, and compilers to spec-driven code generators.

There are many different ways to describe a given program. We get used to thinking of some languages as for writing “implementations” (e.g., Python) and some for writing “specifications” (e.g., various flavors of formal logic). However, I’ve found such a hard-and-fast distinction to be counterproductive. Let’s just think in terms of lower- and higher-level ways to describe functionality.

So the overall idea is that we want to describe programs in as concise, high-level ways as possible. Instead of storing conventional code in repositories, we would prefer to store the highest-level description of requirements that we can get away with, where available tools reliably automate the rest of bringing the desired program to life.

Adam carefully says "ways of describing functionality", but nonfunctional requirements are still in the scope, as they are the real differentiator between specifications and the source code4. If code is transient, specification should describe all required non-functional properties.

Language standards are modest in defining what is observable in the abstract machine. They rarely mention purely nonfunctional properties5 – defining them would require more modeling. Thanks to that omission, compilers, which need to preserve only properties observable in the abstract machine, choose implementations freely, mostly in a deterministic way. Compilation is automatic, cheap, and mostly oversight-free.

Nonfunctional properties are then achieved situationally, and validated for individual artifacts, deployments, contexts. The validation is not universal and persists as long as the context remains. We demonstrate the performance characteristics of this executable, in this deployment, under this workload, sometimes using proxies.

But specifications promise much more. They describe a set of essential functional and nonfunctional properties, and the code generation pipeline is responsible to reliably produce artifacts that satisfy them (unless impossible). Adam writes:

  • A specification is written to explain what functionality is desired, not how to accomplish it. …
  • A specification often includes nondeterminism to provide flexibility to implementers

Nonfunctional properties are not guaranteed unless bound by the specification, and regenerations can arbitarily and liberally change any of them. We can not reliably compile the code and validate nonfunctional properties for the artifact anymore. Instead, we face three burdens:

Burden of model construction
relational properties need environment models to even be expressible;
Burden of articulation
stating required properties;
Burden of adequacy maintenance
keeping models adequate to the world.

Switching from code to specification engineering makes us pay the costs of these burdens (contextual, not necessarily high), and validation may continuously tax us, also requiring human oversight on every regeneration (see previous section). I am not sure if this is often economically attractive.

Are we rich enough to afford cheap code?

Adam writes:

We need to stop thinking of production-ready code as a scarce resource. It may take a few years to get the tools up-to-snuff, but we’ll reach a point where the cost of ongoing reimplementation of significant code bases drops to the levels associated with SaaS subscriptions today.

I agree that implementation becomes cheaper if we generate code from specifications – not as cheap as Adam argues, because of human oversight over regeneration. But implementation step is often not the bottleneck of engineering – the expensive parts are requirement discovery, writing specification, decision making, diagnostics, migration and validation. Especially for systems in an open world, interfacing with other systems, which evolve outside our control.

Complex systems are essentially complex. Changing our approach means redistribution of this complexity. Will it make the expensive parts even more costly, or even unaffordable? Let us go through other aspects of engineering process.

Specification discovery

Engineering software is iterative: implement, run, observe, and adjust the code in response to our discoveries. We discover our intentions and make them more precise. We also discover the world, the real problems that our software is ought to solve, and the connected systems6.

If code is throwaway, we have to keep our discoveries in the specification. Here are some of them:

  1. When we provide a service or a platform, business concerns often force us to accommodate defective behaviors of our clients. We have no control over them, so we do it on our side. NVidia updates drivers frequently to make specific new games perform better, Windows 95 and Joel Spolsky made famous an ad-hoc SimCity fix and modern Windows versions ensure compatibility with older games by applying game-specific "shims", which alter API behavior.

    This complexity is accidental-ish – the games could have been patched if they were in our reach, or if patching was affordable. Boundaries are governed by parties with divergent incentives and update schedules, and coordination can take decades, as we see in the cases of IPv6, or Python 2 to Python 3 migrations.

    These fixes now mud the specification, or some parts of the bundle.

  2. Malicious actors love peeking through leaking abstractions in hopes of discovering another Meltdown or Spectre-level exploit. These exploits emerged when architectural description intentionally abstracted away observable behavior of speculative execution and caches, that can still be harnessed during operation by observing timings and correlating them with data. To reliably prevent similar vulnerabilities from accidentally appearing on regeneration, our bundle might need to include an observational model, and validate its adequacy.

    As a tongue-in-cheek remark, remember how cryptographers extracted RSA secrets using a microphone in 2013? The buzzing frequency of the laptop would be funny to include in the observability model.

    We grow the bundle again, adding another model and validation commitment.

  3. Users grow accustomed to how system looks and feels, to the latency, ordering, messages, visuals, they develop muscle memory, and so on. It is not exactly the case of Hyrum's law – habits are how the system transforms its users7, their response.

    Users like the reduced friction and do not want to break their habits. Persisting code provides some continuity of experience, but a permissive specification only does it accidentally.

    The habits go beyond UX and GUIs. Example: developers use programming languages, compilers adapt to the idiomatic patterns and emit better code for them, then code generators adapt to produce code favorable for compilers. There is a feedback loop.

    Unhappy users are bad for business, so we pump the bunlde with detailed descriptions of the popular workflows.

Open world systems accumulate such sediment. Normally, and Adam seconds this view, we want the specification to be authoritative description of how the system should behave. But, without code, the sediment finds a new home in the specification. The new, mudded specification, describes what the system had to become to fulfill its purpose.

As the specification grows, we engage into familiar engineering practices. Sediment and an overgrown bundle make specification more complex. Abstraction, modularity, hierarchical or layered architectures, standartization, conventions, naming schemes, all the complexity management tricks and programming burdens are back. And to keep complexity locally manageable, the overall complexity of description grows even further. Is complexity easier to manage in the code or in the specification? I do not know.

Debugging becomes harder, and things were not good there to start with.

Diagnostics

One day, after four months of uptime, the generated code crashes, leaving us with a core dump8. Or it just behaves unexpectedly – a "correctly wrong" auction system satisfied fairness and clearing invariants, but permitted an economically catastrophic front-running strategy. Either way, we have to fix the specification, but how exactly? We start investigating.

Detective work

The cause is likely a failure somewhere in the assurance chain:

Assumption violation

We expected our board to operate under temperatures colder than 20°C, but the air got hotter.

The model may have drifted – our board is old and it fails more often than we accounted for in the same temperature. We need to recalibrate.

To facilitate search, we could map generated instructions to the relevant parts of the bundle (specification, models and so on), to ensure reproducible builds, to install monitoring for assumptions, to automatically reconstruct counterexamples for violated assumptions. Adam mentions how proper tooling might help here, and I agree. But the next cases are harder to deal with.

Missing assumption

We forgot a clause: if the air warms up, the board should start throttling.

We did not venture outside the modeled boundary, and we can express the necessary constraint, but we have to figure out the missing constraint first. An engineer will have to do roughly the following:

  • reconstruct the causal execution;
  • distinguish root cause from incidental state;
  • infer what environmental condition was omitted;
  • generalize from the single failure to a revised requirement;
  • decide whether that new requirement should exclude other currently allowed behaviors.

This is interpretive, and humans are unlikely to be fully eliminated from here. A fix might, again, require business- or ethical decision making.

Scope failure

Code lags because of the cache behavior, but our models do not describe cache at all. We need to revise the models.

If the formal language does not have a concept for caches, we may not be able describe prefetching mechanism for the codegen? An engineer will have to do the same work as when facing a missing assumption, but, additionally, they'd have to reason on a meta level to extend the framework, allowing to express the missing constraint.

On a good day we will wrestle with violated assumptions. But sooner or later debugging forces engineers down the abstraction ladder – abstraction leaks universally – especially if the cause is the scope failure. We get our hands dirty with the generated code – and here a permissive specification can make things even more entertaining.

Goldfish debugging

Suppose there is no specification clause that was explicitly violated, and we dive in the generated code. In a day we roughly understand the architecture and what does what, in a week we found the possible root cause – a bug in a third party library, which violates its contract. We adjust and regenerate.

An hour later, another Segmentation fault. We dive back in the code, but it looks completely different. The architecture is not familiar, types enforce different constraints, and the whole error hierarchy and handling is redesigned. Even the stack trace for the crash is unrecognizable! Modification made ripples in the generated code9. We end up spending another two days relearning the codebase before we can investigate again.

There is a similarity between a computer system that provides some service, and a development system – us, engineers. Computers process incoming requests with a required latency – we accept new requirements and adjust the code, meeting deadlines. Consistent low latency requires predictability, so we do our best to engineer systems where interventions have predictable and minimized costs. Volatility translates into unmet deadlines.

But it is hard to intervene without direct control. Reducing memory footprint of a Haskell program is challenging, because all the handles are hidden. For a code generator, controlling algorithms, representations, internal decomposition can be tricky. If its only aim is to satisfy requirements, maybe predictable cost of interventions should also be a requirement. So: additional constraints, lower-level refinements, or extensions to the generation and assurance machinery.

Without limiters, liberal code generation may produce the loss of causal locality, banishing us to debugging hell. The setup for an operational experiment is unstable, the actual system is to rediscover, and discovery is not cheap; for sure it is unpredictable. There will be indeed less memory allocation bugs to debug, but debugging will stay – there are still boundaries, and there is still discovery. Will the net difference in cost be negative? I do not know.

As we wrestle with requirements for months, some of them become confusing. We forget what is the purpose of this or that clause, so we have to reconstruct their origins. Maybe they are not needed anymore? And this brings us to the next problem.

Epistemic decay

All long-lived systems are obscured histories of design decisions. Some ugly corners of legacy systems were reasonable solutions to past tradeoffs, like SimCity fix in Windows 95. Then they blended in, we forgot about them and their purpose, and now if we see one weird bit of code we are often too afraid to get rid of them. Rediscovery is expensive.

Accumulation of illegible historic sediment leads to epistemic decay, I have written extensively about it in my post Vico, Descartes, and decay of knowledge in software. One way of dealing with it is recording decision provenance:

  • the rationale behind the decision;
  • which incident introduced it;
  • which alternatives were rejected;
  • which environmental assumption justified it;
  • who demanded it;
  • which risks were accepted.

If we generate code from specification, the sediment moves to the specification. Specification sediment is different from code sediment.

  1. Code sediment takes part in execution, which is a weak signal for "does this piece of code affect execution anyhow?". A specification clause manifests through its effect on generation, but if it did not affect the current generation, we do not learn much. Maybe it will bind the next one.
  2. Code sediment can be removed, as an experiment. Then we run the code, fuzz it, test it – if something breaks, this is a real signal. But if we remove a clause from specification, we have to regenerate the code. The generator may or may not exploit the new freedom. It may also redesign the rest of the system independently, introducing noise. This is no good diagnostic tool.
  3. The previous point is aggravated by restrictions. Specification may constrain what the generated code should not do, e.g. "implementation for this function should not allocate memory". Code would just not allocate memory and does not record all necessarily rejected alternatives. If we do not record an explicit rationale behind no-allocation, it is hard to get rid of such clause. How do we know it became obsolete?
  4. In return, sediment in specifications is nameable and explicit, so some logical redundancies and inconsistencies can be found in specification automatically. This is good.

My intuition is that switching to specification engineering makes optimization and finding contradictions easier, but deciding what can be safely removed might become hard. But this question warrants a proper research.

The provenance can be partly formalized. Assumptions can be associated with monitors, adaptations to specific clients may be tagged. But rationale – why this reading, what was rejected – is probably natural language and unverifiable. Adam writes:

My edgy claim is that we need to ditch natural language entirely, for periodic regeneration of large code bases to be practical.

Currently, Adam's project is focused on synchronic correctness – implementation should satisfy the current specification. But keeping a specification healthy long term in the open world requires diachronic intelligibility – we have to understand why the specification has its current shape and how it may safely change. I believe we should retain natural language to describe rationale, even if it is eliminated from requirements. Rationale helps getting rid of sediment.

What comes after, or even during debugging? Modify specification, regenerate, redeploy. Is deployment affected as well?

Deployment

Wrong specification can easily lead to an accidentally correct code. Clients do not want us to pad our responses with spaces, but we forgot this requirement; luckily, the generated code does not pad responses anyway. But any regeneration can introduce padding and break the contract. Therefore validation only certifies that the final artifact/deployment demonstrate the validated properties.

Validating the whole system can be expensive. The computer system inside a car comprises hundreds of subsystems and is tested on a series of models, progressively approaching a real car; a full test run may take days. Developers of a gear box do not want to launch the whole test suite on a daily basis. We need some mechanism of evidence transfer – we had evidence that the previous version of artifact demonstrates a property X, something has to assure us that the next version will likely have it too.

Indeed, this is not a new problem, but an extensive use of permissive specifications and code generators might shift the local economy. Specifications bound more properties, code generators make more choices and should keep more promises. The economy has to be carefully investigated.

But the most scary part of the process, in my opinion, comes when deployment is not a mere object replacement, but a surgery on a live patient. Migration of live, stateful systems.

Migration

Adam recognizes that migration is a challenge:

Another concern came up for having tools choose data structures automatically. How does a program evolve over time if the data format keeps changing, leaving prior databases obsolete?

If the representation is derived from the set of constraints in the specification, we'd need to synthesize an automatic data migration protocol between two internal representations of the database. I suppose this might be computationally hard. We can simplify it as Adam suggests, for a price:

This problem is actually addressed pretty naturally: part of the specification for the next version of a program is that it is able to begin with the old contents of a database, where now the specific format of that database is part of the specification of the new version. The code-generation tool may now either keep the database format the same or generate a migration to upgrade to a new representation. (Note that this concern helps us notice a wrinkle of needing to save generated data schemas in version control or similar, even if they were produced automatically.)

Here is a story. There used to be a performance-critical high-load system, with only seconds of downtime acceptable. The legacy time format in its custom database was too narrow to encode the timestamps far in the future, and some clients urgently needed it. Database is changing thousands of times per second, but it has to be migrated on the fly.

Suppose this system were generated from its specification. Following Adam's suggestion we formalize the database layout in the specification – although it brings us down from the desired level of abstraction. We adjust the timestamp format, easy.

But replacing a running stateful system is much, much harder than replacing code and migrating persistent state:

  • in-flight operations must remain valid;
  • rollback must be possible, and may need to transform new state back into an old representation;
  • external obligations must survive;
  • a distributed service may temporarily contain old and new nodes;
  • clients may upgrade on independent schedules;
  • messages produced by an old version may arrive after the new version is deployed;
  • requirements and invariants have to be adjusted and account for the version (before/after);
  • old and new versions of clients will likely coexist
    • and some clients may break – again we have to sort out the behaviors to keep from behaviors to break…

The old system, as specified, should correctly transition into a new system, keeping and adjusting all important properties before, during, and after the transition. To apply formal methods, we'd have to generate a transition system incorporating the implementations before and after the change, live state, deployment policies, and all the connective tissue between the versions. Could we derive this transition system automatically? Would we be able to pay the costs with the lunch money we spared on implementation? I do not know.

Worse: in stateful systems unconstrained regeneration manufactures migrations, unless representations are bound by the specification. Without bounds, rewrite can completely reshuffle the persistent state, which leads to a full-scale migration event. Trying to put this mess under control brings us further from a permissive what-to-do specification and closer to how-to-do specification.

An ongoing migration aggravates any engineering challenge tenfold. Once we switch to specification engineering, our enemies start to masterfully cooperate against us:

  • Debugging is harder, especially when specification formalism can not express a missing clause.
  • Migration is harder, so we will likely have more reasons to debug10.
  • Fixing a problem leads to code regeneration, which might force us to relearn everything, complicating debugging.
  • Migration takes time, and while it is ongoing we might need to initiate another migration – for example, in case we discover a zero-day vulnerability related to the state data layout. How many simultaneous formally verified migrations can we handle?

That timestamp problem, by the way, was not solved through migration. Engineers considered the constraints: tight performance requirements, highly optimized memory layout, inability to stop writes, urgency, and so on. They managed to gather a few unused binary digits scattered around the database record format, then used them for the extra timestamp bits. This clever monstrosity was the price of not migrating the system "properly", and the engineers were happy to pay it.

Concise or permissive specification

Adam acknowledges that Hyrum's law is a challenge for code generation approach:

One interesting question I received was about the place of undocumented features in software that is regularly regenerated. That is, conventional software ships with incidental features that the developers may never have meant to promise to retain indefinitely, and yet users come to depend on them (as laid out in Hyrum’s law). If regeneration can change such incidental features arbitrarily, users may repeatedly be disappointed.

Imagine we generated code from specification for some system that provides a service in the open world. It interfaces with other systems, which evolve independently. It seems that we may not be able to achieve all three properties simultaneously:

  1. a permissive, elegant, universal-quantifier-flavored specification (which Adam wants), and
  2. regeneration freedom (which Adam wants), and
  3. safe compatibility with consequential real contexts.

Compact specification with regeneration freedom (1 and 2) means the system is underspecified and its incidental properties can change at any regeneration. By Hyrum's law all observable properties are potential dependencies. So a client may grow a dependency on some transient property, and then a regeneration breaks compatibility with it.

Adam mentions a possible measure against it:

new releases can be checked against the code of known users, to make sure they remain satisfied in all possible scenarios.

I think this is, in general, unachievable, because the code may depend on non-trivial parts of the behavior e.g. timings or situational response format details, and the introduced incompatibility will be discovered by accident, much later. The formal models may not even have the right ontology to describe such effects (as in the case of acoustic cryptanalysis above).

Inversely, if we keep the specification lean but want to preserve compatibility with other systems, we should not regenerate code liberally and risk changing properties fixed by the artifact but not bound by spec.

And regeneration freedom preserving compatibility means specification will absorb the historical sediment, workarounds, situational fixes and so on – all the operational knowledge to make regeneration safe.

So, there seems to be a trade off in writing specifications:

  • One extreme is a concise and permissive specification. I suspect this is desirable to most people who do formal methods, including Adam. It allows many implementations, some of which may differ in unexpectedly consequential ways. I will argue later that this is problematic for live migrations of stateful systems.
  • Another extreme is a compatibility-complete specification. It captures nearly every observable legacy behavior, but becomes large, historical and restrictive, converging to the source code it specifies.
  • The middle ground is to leave some room for redesign, but to accept compatibility risks.

Let me stress it out again: if we discover incompatibility in the regenerated code, we have to choose which legacy properties to keep and which to abandon. These are often business or ethical decisions, so they should be made by humans. Machines can not even reliably identify them, do not have enough context to solve them and, perhaps, are even fundamentally unfit to make ethical decisions. This conflicts with Adam's idea of no oversight over regeneration.

Conclusion

I like formal methods and in cases like Fiat Cryptography, which are mostly about functional correctness, stateless, S-type systems, generating machine-verified implementations of the clean, concise, small specification is an enthusiastic yes from me.

For other kinds of systems – living in an open world, relying on hardware properties, with extremely complex accurate cost models, with persistent state, interfacing with clients outside our control, accumulating sediment, there are way more complications, hidden costs, and redistribution of complexity to other parts of engineering process.

We may need a stronger evidence that the essential complexity of engineering such systems will not merely be relocated away from the code and towards model engineering, deployment, validation, debugging, requirement discovery, and other, already costly parts of engineering process.

Footnotes:

1

Gilbert Simondon, a remarkable French philosopher of systems, stated that a technical object is not merely the realization of an abstract plan – it individuates through its operation within an associated milieu: other machines, users, physical conditions, maintenance practices and feedback loops. Simondon describes this milieu as part of the technical object’s condition of existence, not an accidental exterior to it. See, for example, "On the Mode of Existence of Technical Objects".

2

For every measurement of resources there are different kinds of performance properties: worst case, average, percentile, amortized… I will consider the worst case bounds here, and leave others out of scope.

3

Crafting models does not mean that we need to create an exact virtual copy of memory controller, or even describe cache hierarchy. The models may only vaguely resemble the objects they model, as long as they are adequate enough to describe important aspects of their behavior.

4

Besides, for any observable resource (like time) we can write code that computes differently based on the resource consumption making functional and nonfunctional aspects of execution fusion. See my post on challenges of specifying and compiling gas-aware languages.

5

Sometimes language standards impose non-functional requirements on the implementation like complexity bounds on standard containers in C++, but they are normative.

6

This mirrors the distinction between Lehman's S-systems and E-systems. Specification is discovered in both cases, but for S-systems the discovery converges, whereas for E-systems the discovery continuously catches up with the changes in the world.

7

Once again, Gilbert Simondon is on point: a system individuates in interactions within its milieu, so as we describe the system in more details, we gradually bring the milieu into description.

8

Formally verified systems can still crash. For example, a 3rd party library violated its contract for which there was no runtime checks, or there is an error in the language semantics, or the world silently drifted away from the formal model.

9

Or maybe the generator was recently updated.

10

Although, again, some classes of bugs will not appear, thanks to formal methods.