why do we invent these formal languages except to be more semantically precise than natural language? What does one gain besides familiarity by translation back into a more ambiguous language?
Mis-defining concepts can be extremely subtle, if you look at the allsome quantifier
https://dwheeler.com/essays/allsome.html you'll see that these problems predate AI, and I struggle to see how natural language is going to help in cases like the "All martians" case where the confusion may be over whether martians exist or not. Something relatively implicit.
We build pretty complex systems only based on "natural language" specifications. I think you are conflating specification ambiguity with verification accessibility.
> What does one gain besides familiarity by translation back into a more ambiguous language?
You gain intent verification. Formal languages are precise about implementation, but they are often opaque about intent. A formal specification can be "precisely wrong". E.g. you can write a perfectly precise Event-B spec that says "When the pedestrian button is pressed, the traffic light turns Green for cars"; the formalism is unambiguous, the logic is sound, the proof holds, but the intent is fatally flawed. Translating this back to natural language ("The system ensures that pressing the button turns the car light green") allows a human to instantly spot the error.
> All Martians are green
Modern LLMs are actually excellent at explicating these edge cases during back-translation if prompted correctly. If the formal spec allows vacuous truth, the back-translation agent can be instructed to explicitly flag existential assumptions. E.g. "For every Martian (assuming at least one exists), the color is Green", or "If there are no Martians, this rule is automatically satisfied". You are not translating back to casual speech; you are translating back to structured, explicit natural language that highlights exactly these kinds of edge cases.
Maybe it can be done, but I struggle to believe adding in that branch for every forall quantifier (which may be plentiful in a proof) is going to help make a proof more understandable. Rather I feel like it'll just balloon the number of words necessary to explain the proof. Feels like it's going to fall on the bad side of verbosity as the sibling comment said.
I think there is a misunderstanding about what is being back-translated.
We don't back-translate the proof steps (the thousands of intermediate logical derivations). That would indeed be verbose and useless.
We back-translate the specification: the Invariants, Guards, and Events.
For a traffic light system, we don't need the LLM to explain the 50 steps of predicate logic that prove inv3 holds. We just need it to translate inv3 itself:
Formal: inv3: light_NS = Green ⇒ light_EW = Red
Back-translation: 'Invariant: If the North-South light is Green, the East-West light MUST be Red.'
This isn't verbose; it's the exact concise summary of the system's safety rules. The 'verbosity' of handling edge cases (like the 'Allsome' example) only applies when the specification itself relies on subtle edge cases, in which case, being verbose is exactly what you want to prevent a hidden bug.
Definitions are built up layer upon layer like an onion too, with each step adding it's own invariants reducing the problem space.
I just feel like the street light example is an extremely small free standing example. Most things that I feel are worth the effort of proving end up huge. Forever formal verification languages were denigrated for being overly rigid and too verbose. I feel like translations into natural language can only increase that if they are accurate.
One thing I wish is this whole discussion was less intertwined with AI.
The semantic gap has existed before AI, and will be run into again without AI.
People have been accidentally proving the wrong thing true or false forever and will never stop with our without AI help.
At the very least we can agree that the problem exists, and while i'm skeptical of natural language as being anything but the problem we ran away from. At least you're trying something and exploring the problem space and that can only be cheered.
My bet is that AI changes the economics of that verbosity, making it cheap to generate and check those 'huge' definitions layer by layer. The next four years will show.
I agree, if AI (or humans) have mistranslated a natural language statement to a formal statement, we should not rely on AI to correctly translate the formal statement back into natural language.
For many statements I expect it's not possible to retain the exact meaning of the formal-language sentence without the natural language becoming at least as complex, and if you don't retain meaning exactly then you're vulnerable to the kind of thing the article warns about.
> if AI (or humans) have mistranslated a natural language statement to a formal statement, we should not rely on AI to correctly translate the formal statement back into natural language.
Perhaps we must not rely on it and find a way to make sure that it cannot fail, but I like to point out that this are two different problems and it seems to me that the current crop of so called AIs are pretty good at distilling excerpts. Perhaps that's the easier problem to solve?
> why do we invent these formal languages except to be more semantically precise than natural language
To be... more precise?
On a more serious note, cannot recommend enough "Exactly: How Precision Engineers Created the Modern World" by Winchester. While the book talks mostly about the precision in mechanical engineering, it made me appreciate _precision_ itself to a greater degree.
Rhetorical sentence? My point is that back-translation into natural langauge is translating into a less precise form. How is that going to help? No number of additional abstraction layers are going to solve human confusion.
> Proprietary use, commercial redistribution, or publishing modified versions with ads or tracking is strictly prohibited under GPLv3 or later.
These all sound to me like "Further restrictions" which the GPL says:
> If the Program as you received it, or any part of it, contains a notice stating that it is governed by this License along with a term that is a further restriction, you may remove that term.
It seems like if you want those clauses that GPL doesn't seem like the license you want?
The reason I included that note is that, as an open-source developer, I’ve seen many projects that weren’t actively maintained get picked up by bad actors as they modify the code and publish it on Google Play with ads or IAPs. I wanted to discourage that.
Other than this notice, MBCompass is fully licensed under GPLv3 or later.
The sum of the note and the gpl doesn't behave as though the notice has any precedence over the gpl. It behaves as additional restrictions and a license that allows you to ignore the additional restrictions. I'm no lawyer but it seems like it isn't achieving what you want.
> I’m planning a non-intrusive in-app prompt to remind users about donations something subtle, because many users forget once they start using the app, rather than only seeing the donation info in the README.
As I mentioned previously, the above approach seems to be well enough and good.
I feel like another optimization that rust code can exploit is uninhabited types.
When combined with generics and sum types these can lead to entire branches being unreachable at the type level. Like Option<!> or Result<T, !>, rust hasn't stablized !, but you can declare them other ways such as an empty enum with no variants.
Sure, in the Result case, less in the option case. I didn't mention it because Infallible is documented and named specifically as an Error "The error type for errors that can never happen". The use of uninhabited types as an unreachable code optimization is useful beyond errors though.
I always feel that when saying lex/yacc style tools, it comes with a lot of preconceived notions that using the tools involves a slow development cycle with code gen + compilation steps.
What drew me to the grmtools (eventually contributing to it) was that you can evaluate grammars basically like an interpreter without going through that compilation process.
Leading to a fairly quick turnaround times during language development process.
I hope this year I can work on porting my grmtools based LSP to browser/wasm.
I couldn't agree with you more, the thing is our underlying security models are
protecting systems from their users, but do nothing for protecting user data from the programs they run. Capability based security model will fix that.
Only on desktop. Mobile has this sorted. Programs have access to their own files unrestricted, and then can access the shared file space only through the users specifically selecting them.
I think there's 2 kinds of systems we're talking about here:
1. Capabilities given to a program by the user. Eg, "This program wants to access your contacts. Allow / deny". But everything within a program might still have undifferentiated access. This requires support from the operating system to restrict what a program can do. This exists today in iOS and Android.
2. Capabilities within a program. So, if I call a function in a 3rd party library with the signature add(int, int), it can't access the filesystem or open network connections or access any data thats not in its argument list. Enforcing this would require support from the programming language, not the operating system. I don't know of any programming languages today which do this. C and Rust both fail here, as any function in the program can access the memory space of the entire program and make arbitrary syscalls.
Application level permissions are a good start. But we need the second kind of fine-grained capabilities to protect us from malicious packages in npm, pip and cargo.
I would also say there is a 3rd class, which are distributed capabilities.
When you look at a mobile program such as the GadgetBridge which is synchronizing data between a mobile device and a watch, and number of permissions it requires
like contacts, bluetooth pairing, notifications, yadda yadda the list goes on.
Systems like E-Lang wouldn't bundle all these up into a single application. Your watch would have some capabilities, and those would interact directly with capabilities on the phone. I feel like if you want to look at our current popular mobile OS's as capability systems the capabilities are pretty coarse grained.
One thing I would add about compilers, npm, pip, cargo. Is that compilers are transformational programs, they really only need read and write access to a finite set of input, and output. In that sense, even capabilities are overkill because honestly they only need the bare minimum of IO, a batch processing system could do better than our mainstream OS security model.
I'd also note capros doesn't fit that description either.
I don't know that there were examples that ran more than a single process.
That's probably not true, for anything relying on drivers since user mode drivers are basically processes there... but in the way that people might think of a process.
I mean, there isn't exactly a thriving ecosystem of existing software built for CapROS. Right now I don't think anybody even has CapROS itself building.
The problem has gotten a lot easier since the EROS days, thanks to Xen, QEMU, UEFI (?), and the explosion of cheap hardware, but it looks like maybe Charlie got sick or lost interest or something?
Yeah, I did see a email on a capabilities list from him about him no longer working on it because of lack of feedback & wanting to just enjoy his retirement. That was the impression I got.
When he had resumed his work on it, I personally had been going through a back injury. I still feel bad that I didn't get a chance to contribute any of the hardware ports and software I wrote for it.
I wasn't able to google it, or find a public link to the email (but it was posted on a public list) so here is some relevant snippets from it.
Nov 20 2022 titled CapROS status
"When I retired a year ago I hoped to correct some of those issues, but I want to enjoy retirement and not just have a full-time unpaid job.", ...
"I am considering just abandoning CapROS. I believe there are some useful ideas in the system, but so far no one seems to have known or cared about them."
Yes, 50 years of LCF would have been much better. You should not talk about "50 years of proof assistants" and not mention Mizar which had the largest library of theorems for about half of that time.
Without the low int the even/odd theorem falls apart for wrap around
I've definitely seen algorithms that rely upon that.
I would agree, whether error values are in or out of band is pretty context dependent
such as whether you answered a homework question wrong, or your dog ate it.
One is not a condition that can be graded.
Meh, you also see algorithms that have subtle bugs because the author assumed that for every integer x, -x has the same absolute value and opposite sign.
I view both of these as not great. If you strictly want to rely on wraparound behavior, ideally you specify exactly how you're planning to wrap around in the code.
that all integers are either even or odd, and that for an even integer that integer + 1 and - 1 are odd and vice versa for odd numbers. That the negative numbers have an additional digit from the positive numbers ensures that low(integer) and high(integer) have different parity. So when you wrap around with overflow or underflow you continue to transition from an even to odd, or odd to even.
Presumably since this language isn't C they can define it however they want to, for instance in rust std::i32::MIN.wrapping_sub(1) is a perfectly valid number.
Back when those machines existed, UB meant "the precise behaviour is not specified by the standard, the specific compiler for the specific machine chooses what happens" rather than the modern "a well-formed program does not invoke UB". For what it is worth, I compile all my code with -fwrapv et. al.
My feeling is that languages with other packing models are merely less convenient,
and there is no actual tangible difference security-wise. Just take C and replace "look for writable repositories". It just takes more work and is less uniform to say write a worm that looks for writable cmake/autoconf and replicate that way.
What would actually stop this is writing compilers and build systems in a way that isolates builds from one another. It's kind of stupid that all a compiler really needs is an input file, a list of dependencies, and an output file. Yet they all make it easy to root around, replicate and exfiltrate. It can be both convenient and not suffer from these style of attacks.
Not really. cmake and automake are for compiling the library, not for the downloading it. The gap between the two is what's get erased from npm. And it made worse because of the auto update set by default when `npm install` is run.
Seems doubtful, given that generics and the gccgo compiler were both spearheaded by Ian Lance Taylor, it seems more likely to me that him leaving google would be a more likely suspect, but I don't track go.
Mis-defining concepts can be extremely subtle, if you look at the allsome quantifier https://dwheeler.com/essays/allsome.html you'll see that these problems predate AI, and I struggle to see how natural language is going to help in cases like the "All martians" case where the confusion may be over whether martians exist or not. Something relatively implicit.
reply