I’m really interested in the logic behind this. Why would we take a bottom up approach to correctness instead of a top down approach?
From my perspective, these downstream concerns become easier to solve once correctness can be verified on an ongoing basis.
Eh. There is no formalized way to prove correctness in languages beyond Idris/Lean/Agda circle.
Yet there is a way to prove some parts of it, like using best abstractions, minimizing the approximate size of a function on a domain, and whatnot static analyzers can analyze.
That’s why we use existing tools rather than dream about not only inexisting, but generally impossible ones.
I think we’re coming at correctness from two different perspectives.
You’re treating it as an engineering concern - whether we can statically prove properties of the code itself. And you’re right that outside the Idris/Lean/Agda circle, formal program correctness is largely out of reach.
I’m treating it as an operational concern - does the application do what it was designed to do? Not what it does mechanically, but whether it actually does the thing the user asked for. That’s a different question. I wouldn’t try to answer it with static analysis. I’d answer it with executable acceptance criteria that get re-verified on every commit.
So when I say “correctness first,” I’m not asking for a tool that proves all code in some general sense. I’m asking for a way to keep the application bound to the intent it was built to satisfy. The downstream concerns (architecture, security, code quality) get much easier to address once you can verify intent on an ongoing basis - because they’re no longer load-bearing for whether the thing works.
Either you are The Keeper of Secret Knowledge, or you are a modest Santa Claus believer. The closest attempt to come up with some acceptance criteria was done 23 years ago and is now known as property-based testing (originally QuickCheck by John Hughes and Co.)
We probably have to define a failure cost for a domain we are talking about. I use to work in industries, where one unexpected race condition (I hope it’s obvious that race condition cannot be caught by “acceptance testing”) might cost $Ms. On the other hand, if the failure cost is “one annoyed user,” I don’t see any reason to test the code whatsoever.
This is a great point. I’m not totally sure how to do this objectively, but the value is self-evident.
Property-based testing and testable acceptance criteria are different abstraction layers. Property-based testing is great for domain invariants, but acceptance criteria are there for binding user intent to verification. They do different jobs.
And you’re 100% correct. Acceptance testing won’t catch race conditions, and those are targets for different kinds of testing. Acceptance testing doesn’t replace the lower-level unit and property-based testing. It sits above it and ensures the application does what the end user is asking for.
This conversation even further drives home the need for bucketing. When I say correctness and you say correctness, we’re talking about two different things. Do you think there’s a better word for the type of correctness I’m proposing? Because I think I’m misusing the term.
To me there is a clear divide between application quality and code quality. The requirements and specifications might ask for a horrible application with bad UI, but the code to do so can be high quality. Thus I suggest limiting this to code quality as such.
I agree code quality consists of many themes, and splitting into subthemes or buckets make sense to me. But I also think of meeting requirements and specifications as the critical critiera. To me the others are means to that end although with maintainability and future evolution in mind.
Clearly cost of failure is important, and what is the optimal balance of code cost and risk level varies with different projects. But does it change the definitions of what quality code is? Or is it more a question of how high up the same quality ladder a certain risk level warrants?
(Edit: A ladder is too one-dimensional, but if quality has different quality axis then those definitions are there independent of where a specific needed solution might point?)
I know what acceptance testing is. My point is it’s meaningless in a vast majority of cases.
A mediocre developer is usually able to cover happy-path cases, and acceptance testing is all about happy-path. Unhappy path, though, involves race conditions, network splits, power outages, and whatnot.
I think we might be disagreeing about what acceptance testing is for in this context.
In a traditional development model, humans write the code and the tests, and the tests check that the intent matches the output. You’re right that this biases toward happy paths.
Part of what makes a BDD spec a good BDD spec is that it covers both the happy path and the unhappy path by construction. Validation failures, permission denials, missing-data edge cases, “should not happen” negatives - those all live in the scenarios, not as an afterthought.
When you’re generating large amounts of code or a full application, that’s where the inversion kicks in. The scenarios are written first, and they do two jobs at once: they communicate the designer’s intent to the model, and they verify the intent has been met (assuming the proper constraints have been applied to the test suite). The developer’s job becomes “author comprehensive scenarios.” The agent’s job is “pass them all.” If you want unhappy-path coverage, you write scenarios for it, and the agent builds to those scenarios.
Acceptance tests are not going to cover the difficult scenarios you proposed - race conditions, network splits, power outages. That doesn’t make them wrong. It’s a different tool for a different job.
I think we’re saying the same thing from different starting points. Your application-quality / code-quality split is the same line I’m drawing with correctness vs the other buckets. It’s a different vocabulary but the same concept.
You’re right that meeting requirements is the critical criterion, and architecture / security / code quality are means to that end. I don’t think you can evaluate code quality well without keeping application quality in view. Code quality is in service of application quality.
Failure cost doesn’t change the definitions, it changes where you apply which tools in the harness. Originally I had the harness generating module specs with engineering guidance for each module, unit tests asserting properties about each module, and then the implementation. In my most recent experiment I only generated BDD specs and code, and that was enough to get a working full application across the line. That’s the example of optimizing on “application correctness” over any other concern.
The next step from there is going back in selectively and adding unit tests and module specs to the critical portions where the failure cost warrants the extra rigor. Not every module needs that level of discipline; some absolutely do. Same buckets, different rigor per part of the codebase.
Yes, it seem we think a lot alike except in different terms.
Application quality often introduces matters of taste in UI, workflow preferences and various other metrics that exists outside of code quality as I think of it. My thinking is that the requirements and specifications is the contract for the code, and whether the application is worthwhile or not is not a code quality issue as such.
Failure risk decides the specification, and the specification guides the needed (possibly verifiable) quality. And that includes choice of language, architecture and hardware as well. Elixir will not be right for everything, and that is fair enough. I’ve used finite state machines with redundant parallel FGPA processes back in the day, and others might have legal requirements for formal verifiable solutions. But within what Elixir do cover, it should be possible to have some definitions of quality to optimize code generation and tests for. (And then it would be up to specifications to decide what level a given application need).