@gavin.codes
In the very near future code will be organised more around contract than implementation, just as currently we organise around high-level constructs and not machine code.
December 11, 2025 at 7:34 AM
In the very near future code will be organised more around contract than implementation, just as currently we organise around high-level constructs and not machine code.
Generative AI is finally making software verification not just practical, but it a requirement (pun intended). AI slop is a serious problem, but it is also an opportunity.
December 11, 2025 at 7:34 AM
Generative AI is finally making software verification not just practical, but it a requirement (pun intended). AI slop is a serious problem, but it is also an opportunity.
At bookwyrm.ai we've been performing experiments in Neural-symbolic programming and we're getting amazing results. Generative AI driven by both specification and formal verification.
December 11, 2025 at 7:34 AM
At bookwyrm.ai we've been performing experiments in Neural-symbolic programming and we're getting amazing results. Generative AI driven by both specification and formal verification.
7/
And lo and behold, during my exploration of the space of tools to assist in this I found that Bertrand Meyer the author of DbC has been thinking along very similar lines and has made the case in a pre-print! se.inf.ethz.ch/~meyer/publi...
And lo and behold, during my exploration of the space of tools to assist in this I found that Bertrand Meyer the author of DbC has been thinking along very similar lines and has made the case in a pre-print! se.inf.ethz.ch/~meyer/publi...
December 9, 2025 at 8:34 AM
7/
And lo and behold, during my exploration of the space of tools to assist in this I found that Bertrand Meyer the author of DbC has been thinking along very similar lines and has made the case in a pre-print! se.inf.ethz.ch/~meyer/publi...
And lo and behold, during my exploration of the space of tools to assist in this I found that Bertrand Meyer the author of DbC has been thinking along very similar lines and has made the case in a pre-print! se.inf.ethz.ch/~meyer/publi...
6/
Step A improves discoverability of code for re-use by the LLM. Step D reduces the burden on programmers to ensure correctness. Both address serious problems with current vibe-coding practices.
Step A improves discoverability of code for re-use by the LLM. Step D reduces the burden on programmers to ensure correctness. Both address serious problems with current vibe-coding practices.
December 9, 2025 at 8:34 AM
6/
Step A improves discoverability of code for re-use by the LLM. Step D reduces the burden on programmers to ensure correctness. Both address serious problems with current vibe-coding practices.
Step A improves discoverability of code for re-use by the LLM. Step D reduces the burden on programmers to ensure correctness. Both address serious problems with current vibe-coding practices.
5/
D) Use the contracts for static and dynamic verification. The boolean specifications can be used to do hypothesis testing we can derive test data (and therefore tests) automatically. SMT solvers can be used to check pre-post conditions.
D) Use the contracts for static and dynamic verification. The boolean specifications can be used to do hypothesis testing we can derive test data (and therefore tests) automatically. SMT solvers can be used to check pre-post conditions.
December 9, 2025 at 8:34 AM
5/
D) Use the contracts for static and dynamic verification. The boolean specifications can be used to do hypothesis testing we can derive test data (and therefore tests) automatically. SMT solvers can be used to check pre-post conditions.
D) Use the contracts for static and dynamic verification. The boolean specifications can be used to do hypothesis testing we can derive test data (and therefore tests) automatically. SMT solvers can be used to check pre-post conditions.
4/
C) Have an LLM write the implementation. With a combination of editor mode fencing which stops the LLM from editing the specification we can drive an LLM with a very explicit definition of correctness helping it to get the correct answer.
C) Have an LLM write the implementation. With a combination of editor mode fencing which stops the LLM from editing the specification we can drive an LLM with a very explicit definition of correctness helping it to get the correct answer.
December 9, 2025 at 8:34 AM
4/
C) Have an LLM write the implementation. With a combination of editor mode fencing which stops the LLM from editing the specification we can drive an LLM with a very explicit definition of correctness helping it to get the correct answer.
C) Have an LLM write the implementation. With a combination of editor mode fencing which stops the LLM from editing the specification we can drive an LLM with a very explicit definition of correctness helping it to get the correct answer.
3/
B) Write predicates which check the conditions of the contract (pre/post-conditions and invariants). In my experiments I have used python itself to define boolean functions which act as predicates.
B) Write predicates which check the conditions of the contract (pre/post-conditions and invariants). In my experiments I have used python itself to define boolean functions which act as predicates.
December 9, 2025 at 8:34 AM
3/
B) Write predicates which check the conditions of the contract (pre/post-conditions and invariants). In my experiments I have used python itself to define boolean functions which act as predicates.
B) Write predicates which check the conditions of the contract (pre/post-conditions and invariants). In my experiments I have used python itself to define boolean functions which act as predicates.
2/
A) Write contracts in conversation with an LLM to improve requirements gathering and specification completeness. LLMs are quite good at getting people to clarify written text and can accelerate things substantially.
A) Write contracts in conversation with an LLM to improve requirements gathering and specification completeness. LLMs are quite good at getting people to clarify written text and can accelerate things substantially.
December 9, 2025 at 8:34 AM
2/
A) Write contracts in conversation with an LLM to improve requirements gathering and specification completeness. LLMs are quite good at getting people to clarify written text and can accelerate things substantially.
A) Write contracts in conversation with an LLM to improve requirements gathering and specification completeness. LLMs are quite good at getting people to clarify written text and can accelerate things substantially.
🧵1/
I've been conducting experiments with the use of LLMs for "Design by Contract" (DbC), a paradigm described by Bertrand Meyer. DbC is quite straightforward to use in a language like python (for instance using icontract). The idea is essentially to:
I've been conducting experiments with the use of LLMs for "Design by Contract" (DbC), a paradigm described by Bertrand Meyer. DbC is quite straightforward to use in a language like python (for instance using icontract). The idea is essentially to:
December 9, 2025 at 8:34 AM
🧵1/
I've been conducting experiments with the use of LLMs for "Design by Contract" (DbC), a paradigm described by Bertrand Meyer. DbC is quite straightforward to use in a language like python (for instance using icontract). The idea is essentially to:
I've been conducting experiments with the use of LLMs for "Design by Contract" (DbC), a paradigm described by Bertrand Meyer. DbC is quite straightforward to use in a language like python (for instance using icontract). The idea is essentially to:
6/ We've a chicken-and-egg type situation at the minute. Probably python will continue to be optimal in that you can add type annotations while not requiring type discipline while also getting some advantages of static analysis.
December 4, 2025 at 12:45 PM
6/ We've a chicken-and-egg type situation at the minute. Probably python will continue to be optimal in that you can add type annotations while not requiring type discipline while also getting some advantages of static analysis.
5/ Types are also of interest. While types make it harder for AIs to one shot (they require more loops) they tend to get better code and the types themselves tend to constrain the output to more *correct* code.
I'm having trouble finding proof of this in the literature.
I'm having trouble finding proof of this in the literature.
December 4, 2025 at 12:45 PM
5/ Types are also of interest. While types make it harder for AIs to one shot (they require more loops) they tend to get better code and the types themselves tend to constrain the output to more *correct* code.
I'm having trouble finding proof of this in the literature.
I'm having trouble finding proof of this in the literature.
4/ This suggests that the semantics of javascript are inherently more complex for LLMs to get a handle on since the volumes must be very high. It could well be that typescript just doesn't have enough data to fix the problem.
December 4, 2025 at 12:45 PM
4/ This suggests that the semantics of javascript are inherently more complex for LLMs to get a handle on since the volumes must be very high. It could well be that typescript just doesn't have enough data to fix the problem.
2/ Volume is key to training AIs, and so those programming languages with large training volumes tend to win. Python is killing it. However there are some secrets hidden in this chart.
December 4, 2025 at 12:45 PM
2/ Volume is key to training AIs, and so those programming languages with large training volumes tend to win. Python is killing it. However there are some secrets hidden in this chart.
1/ If you're using AIs to generate code, you might want to have a look at this chart. Language choice now should also take into account AI comprehension and writing abilities.
December 4, 2025 at 12:45 PM
1/ If you're using AIs to generate code, you might want to have a look at this chart. Language choice now should also take into account AI comprehension and writing abilities.
9/ And best of all the entire methodology through step 7 can be treated as a kind of increasing level of trust in the software without us having to pay human attention much beyond the logical contract.
December 1, 2025 at 4:01 PM
9/ And best of all the entire methodology through step 7 can be treated as a kind of increasing level of trust in the software without us having to pay human attention much beyond the logical contract.
6/ It's worth recalling a claim of two famous MIT professors
"Computer science is not a science, and its ultimate significance has little to do with computers" — Abelson / Sussman
"Computer science is not a science, and its ultimate significance has little to do with computers" — Abelson / Sussman
November 28, 2025 at 7:55 AM
6/ It's worth recalling a claim of two famous MIT professors
"Computer science is not a science, and its ultimate significance has little to do with computers" — Abelson / Sussman
"Computer science is not a science, and its ultimate significance has little to do with computers" — Abelson / Sussman
5/ Two contenders for a basic foundation which can be used as hand written pseudocode that strike me are Z-notation and APL.
Probably we would need to adapt approaches but these are compact enough and mathematical enough that they can do the job.
Image
Probably we would need to adapt approaches but these are compact enough and mathematical enough that they can do the job.
Image
November 28, 2025 at 7:55 AM
5/ Two contenders for a basic foundation which can be used as hand written pseudocode that strike me are Z-notation and APL.
Probably we would need to adapt approaches but these are compact enough and mathematical enough that they can do the job.
Image
Probably we would need to adapt approaches but these are compact enough and mathematical enough that they can do the job.
Image
4/ I've been putting some thought into how the curriculum would have to change — typical programming languages are largely too verbose to comfortably write on the blackboard or with pen.
November 28, 2025 at 7:55 AM
4/ I've been putting some thought into how the curriculum would have to change — typical programming languages are largely too verbose to comfortably write on the blackboard or with pen.
3/ Before students learn to drive an AI to assist in programming, they need a firm grasp of deep concepts in CS. Algorithms, relationship between proof and algorithms and complexity theory.
November 28, 2025 at 7:55 AM
3/ Before students learn to drive an AI to assist in programming, they need a firm grasp of deep concepts in CS. Algorithms, relationship between proof and algorithms and complexity theory.
2/ AI presents too many opportunities for laziness. As long as assignments are on computer there is no way we can avoid the use of AI to do the assignments. If the assignment is a lot of boilerplate (which humans will no longer do) then this is useless learning for the AI age.
November 28, 2025 at 7:55 AM
2/ AI presents too many opportunities for laziness. As long as assignments are on computer there is no way we can avoid the use of AI to do the assignments. If the assignment is a lot of boilerplate (which humans will no longer do) then this is useless learning for the AI age.
1/ I used to lecture in CS. Due to AI, I can tell you if I did it now I would not allow any computers in my class room at all. Assignments would be pen and paper. Students need to learn to reason, first and foremost.
November 28, 2025 at 7:55 AM
1/ I used to lecture in CS. Due to AI, I can tell you if I did it now I would not allow any computers in my class room at all. Assignments would be pen and paper. Students need to learn to reason, first and foremost.
6/ Going to a complete liquid metal fuel might be viable for other fuel arrangements which are not so useful for bombs. In addition Fast reactors can run on nuclear waste, reprocessed from other reactors which can eliminate one of the great bug-bears of the nuclear solution: waste.
November 26, 2025 at 11:12 AM
6/ Going to a complete liquid metal fuel might be viable for other fuel arrangements which are not so useful for bombs. In addition Fast reactors can run on nuclear waste, reprocessed from other reactors which can eliminate one of the great bug-bears of the nuclear solution: waste.
5/ Maybe having a liquid plutonium core reactor is a bit crazy - it certainly violates any modern concept of non-proliferation! However the ideas contained here are interesting none-the-less.
November 26, 2025 at 11:12 AM
5/ Maybe having a liquid plutonium core reactor is a bit crazy - it certainly violates any modern concept of non-proliferation! However the ideas contained here are interesting none-the-less.
4/ These advantage of such a fast reactor is that the increasing heat induces a negative reactivity response, as the fuel expands. This helps to make the reactor passively self-stabilising.
November 26, 2025 at 11:12 AM
4/ These advantage of such a fast reactor is that the increasing heat induces a negative reactivity response, as the fuel expands. This helps to make the reactor passively self-stabilising.