My [interpretation? fanfic?] is that Julia is like a carnivore, and humanity is not it's first prey. Every creature that eats, eats to steal the disentropy of it's meal. Plants can steal order from sunlight, and certain microbes can steal order from thermal vents, but carnivores, herbivores, and decomposers steal order from the work of other organisms. The improbability of living is sustained by arranging stolen amino acids into one's own proteins, powered by the toppleing of sugar towers back into a jumbled mess.
Julia does not reassemble amino acids like earth life does. But it does absorb disentropy from it's prey. The extreme specificity of an interstellar spacecraft, it's contents and occupants, is absorbed by Julia, so that it can move, grow, and attract more prey.
Decidability is of academic interest, and might be a hint if something is feasible.
But there are (1) ways of sidestepping undecidability, e.g. A valid C++/Rust program is one for which the typechecker terminates in x steps without overflowing the stack
And (2) things which are decidable, but physically impossible to calculate, e.g the last digit of the 10^10^10 th prime
What matters is being able to reject all incorrect programs, and accept most human written valid programs
Decidability of a type system is like well-typedness of a program. It doesn't guarantee it's sensible, but not having the property is an indicator of problems.
I'm not entirely smart enough to connect all of these things together but I think there is a kind of subtlety here thats being stepped on.
1. Complete, Decidable, Well founded are all distinct things.
2. Zig (which allows types to be types) is Turing complete at compile time regardless. So the compiler isn't guaranteed to halt regardless and it doesn't practically matter.
3. The existance of a set x contains x is not enough by itself to create a paradox and prove false. All it does is violate the axiom of foundation, not create a russles paradox.
4. The axiom of foundation is a weird sort of arbitrariness in that it implies this sort of DAG nature to all sets under set membership operation.
6. The Axiom of Foundation exists to stop you from making weird cycles, but there is parallel to the axiom of choice, which directly asserts the existance of non computable sets using a non algorithmicly realizable oracle anyway....
Your other points are more relevant to the content of the article, but point 2. relates the practical consequences of undecidable type-checking, so I'll reply to that.
I don't have a problem with compile time code execution potentially not terminating, since it's clear to the programmer why that may happen. However, conventional type checking/inference is more like solving a system of constraints, and the programmer should understand what the constraints mean, but not need to know how the constraint solver (type checker) operates. If it's undecidable, that means there is a program that a programmer knows should type check, but the implementation won't be happy with; ruining the programmer's blissful ignorance of the internals.
> 2. Zig (which allows types to be types) is Turing complete at compile time regardless. So the compiler isn't guaranteed to halt regardless and it doesn't practically matter.
Being Turing complete at compile time causes the same kinds of problems as undecidable typechecking, sure. That doesn't make either of those things a good idea.
> 3. The existance of a set x contains x is not enough by itself to create a paradox and prove false. All it does is violate the axiom of foundation, not create a russles paradox.
A set that violates an axiom is immediately a paradox from which you can prove anything. See the principle of explosion.
> 4. The axiom of foundation is a weird sort of arbitrariness in that it implies this sort of DAG nature to all sets under set membership operation.
Well, sure, that's what a set is. I don't think it's weird; quite the opposite,
> 5. This isn't nessesarily some axiomatically self evident fact. Aczel's anti foundation axiom works as well and you can make arbitrary sets with weird memberships if you adopt that.
I don't think this kind of thing is established enough to say that it works well. There aren't enough people working on those non-standard axioms and theories to conclude that they're practical or meet our intuitions.
> 6. The Axiom of Foundation exists to stop you from making weird cycles, but there is parallel to the axiom of choice, which directly asserts the existance of non computable sets using a non algorithmicly realizable oracle anyway....
The Axiom of Foundation exists to make induction work, and so does the Axiom of Choice. They both express a sense that if you can start and you can always make progress, eventually you can finish. It's very hard to prove general results without them.
But like, of all the
expressive power vs analyzability
trade-offs you can make,
there's a huge leap in expressive power
when you give away decidability.
Undecidability is not a sign
that the foundation has cracks
(not well founded),
but it might be a sign
that you put the foundation on wheels
so you can drive it at highway speeds,
with all the dangers that entails.
It's not a trade everyone would make,
but the languages I prefer do.
jukebox? jeux is found by my solver, although I'm not sure Sam would include it. I'm working on a site for solving Spelling Bee, Letter Boxed, Strands, etc.
What was your algorithm? Compute a bitset for every word, for each word with 7 unique letters, check against every other word if it has a subset of those letters? Surely there's a better than O(n^2) way
Start with your chosen dictionary, remove small words and all 's'es.
Then find all words with 7 unique letters, then get the unique set of letter sets. These are your valid puzzles times 7 for each selection of a center letter.
Construct a trie of your dictionary. For each letter of each puzzle, walk the trie using only the puzzle letters. When you find a word, if it used the center letter, add to list.
~I watched a video series where someone did the techniques in isolation in reverse order and I thought it was a good idea. That way you're always learning on perfect ingredients. i.e. buy chips and learn to temper, then buy roasted nibs and learn to refine, then buy dried and learn to roast, then buy pods and learn to ferment and dry.~
Is anyone working on applying these techniques to formal verification of software?
My limited understanding of Rust is that it applies a fixed set of rules to guarantee memory safety. The rules are somewhat simple and limiting, for ease of understanding and implementation, but also because of undecidability.
Programmers run into situations where they know that their code won't cause memory errors, but it doesn't follow the rules. Wouldn't it be cool if something like Aristotle was integrated into the compiler? Any code for which a proof of correctness could be written would pass/compile, without having to add more and more rules
Formal methods are cool because, by contrast to tools like the borrow checker, you can prove some very "nonlocal" properties: this system does not deadlock, or it makes progress at least every N steps, etc.
TLA+ is generally used to specify a "toy model" of some complex distributed system. It's not intended for end-to-end proof, for that you'd just use Coq/Rocq or Lean itself. Lean is certainly expressive enough, but you'll have to translate the time and non-determinism modalities of TLA+ as part of the Lean development.
We can't know for every possible program if it halts or not, but the complexity of programs we can determine is increasing as tools and techniques get better
An issue with this approach is that it may not be robust. That is, you could run into a casr where a minor modification of your program is suddenly not provable anymore, even though it is still correct. The heuristic (AI or otherwise) has necessarily limits, and if your are close to the "edge" of its capabilities then a minor change could push it across.
If the proof is rooted in the programmer's understanding who can give proof hints to the prover then any modification of the program can then be accompanied with a modification of the hints, still allowing automatic proofs. But if the human has no clue then the automatic system can get stuck without the human having a chance to help it along.
The same is true for optimization. One small change and the compiler's optimizer doesn't know anymore how to optimize the code, and your code is now slow. And there is no way for a programmer to fix it except by rolling back their changes or by inspecting the assembly output.
Formal verification of program correctness is also (for obvious reasons) key to unlocking AI-driven synthesis (i.e. 'vibe' coding) of "correct" programs that will verifiably meet the given spec.
It will certainly help - but its an extremely high bar. Almost all formal verification of software today is "does this pass the typechecker"?.
Now this captures some errors, but it doesn't really capture high level ones (is this program guaranteed to not deadlock is a hard one), and it doesn't capture the one that is important for business purposes (does this do what the customer wants). That requirement is more important than correctness (vitness all the software that is described as "crap", but is nonetheless widely used).
I don't think this is a required key to unlocking vibe coding. That seems to be easy: does this provide business value? And there the answer seems roughly to be "yes".
Not all aspects of a spec can be formally encoded. But even half-way houses are good.
Eg you can give the vague spec 'build me a todo list app', but you can still formally prove that everything your app does finishes, or even that it finishes in reasonable time.
Yes. For sure we will never be able to 100% automate the whole SWE process. As you say, the first input is a human wish, and there comes the joke of the genie that always screw the wishes by leaving something obvious out, because not explicitly specified. Also I think at some point the halting problem will make some programs impossible to test. But it would so great, program in a loose syntax, but with more safety than Rust and Ada together
> Also I think at some point the halting problem will make some programs impossible to test.
No, not at all. The halting problem isn't much of a problem here.
To elaborate: yes, it's pretty much impossible to decide whether an arbitrary programme will halt. But we aren't dealing with arbitrary programmes, you carefully have your agent craft programmes that are easy to prove correct.
There are languages available today whose type systems already only let you write terminating programmes. See eg https://news.ycombinator.com/item?id=32102203 the Dhall language. Or Agda or Lean itself (unless you specifically opt out via the 'partial' keyword. But it's trivial to check whether someone used 'partial'.)
If your agent write a programme that's not easy to prove to be terminating, you don't try harder to prove. You just flag that as an error and have the agent try again.
Just like as a human code reviewer you reject Pull Requests that are too complicated to understand: you don't even bother figuring out whether they are technically correct or not.
Thanks. I expressed it with doubt, because I assume there had to be some way around.
If I understood correctly, the halting problem states you cannot make a program to test any program. But you can do if you test a relatively small, possibly finite and well defined subset of programs, right?
> If I understood correctly, the halting problem states you cannot make a program to test any program. But you can do if you test a relatively small, possibly finite and well defined subset of programs, right?
In the standard theories everything becomes trivial, if you go finite.
The trick is not so much that you have a well-defined subset, but that you allow your programme analyser to say 'Eh, I don't know'.
The halting problem is impossible to solve in general, if you analyser has to answer "Definitely halts" or "Definitely runs forever" for any given programme you present it with. If you give a third option "Eh, I don't know", you can solve the problem.
Trivially you might always say "Eh, I don't know" and never be wrong. But we can write useful analysers that try their best not to say "Eh, I don't know".
One example is type checkers in compilers. When they detect that you are eg trying to add numbers and strings, then something is definitely wrong with your programme. But when they let your programme through, it doesn't mean your programme is flawless.
The opposite is what you get with prove assistants like we were discussing: if they prove your programme correct, it's definitely according to the specs. But if the fail, that doesn't mean that your programme is definitely incorrect; they might have just failed to find a proof.
There doesn't need to be a need and simple definition of programmes your theorem prover works vs fails on. Eg if you upgrade the AI agent that helps you find the proof (or hire a smarter human to drive it) they might suddenly find a proof where they struggled previously.
Imagine fearing the consequences of "people are not gay by choice, but because they are each halves of a eight limbed cartwheeling sphere". Young minds cannot handle such dangerous rhetoric
reply