The surface of bugs in Lean is infinitely smaller than the human error involeved in a committee of peer reviewers. It's way more probable to say "it's proven because Lean says so" than "it's proven because a couple of reviewers said so".
Also, if a bug is found, all previosuly proven theorems can be reproven to immediately and conclusively find out if things went wrong somewhere
Godel proved that any system expressive enough to produce an arithmetic is incomplete. He initially proved it for the peano axioms but then it got generalized. ZFC can produce an arithmetic. Also, before being arrogant and demanding explanations, you should give them first for your claims
you understand that "expressive enough to produce" are not obvious elements of zfc, that's some average consumer napkin math and not strict formalization.
That increases the likelihood that they are right.
> support your point with explanation or be ignored :-)
Anyone who says "Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems" and isn't joking warrants a permanent ignore.
A quick google search shows different proof assistants have been used to obtain the Peano axioms from ZFC, such as Isabelle/ZF and Metamath. I think you're just wrong
coming back to your argument about peano being obtained from zfc, you obviously can't prove that it happened using purely zfc, and not some logical framework embedded into those proof assistants.
I said I am not expert, I am indeed not expert in zfc and godel theorems, but I am an expert (phd) in actual formalization theory.
Formal theory is very simple concept: its alphabet, set of formulas on top of this alphabet, and function which translates one formula to another.
ZFC can't "obtain" peano, simply because it doesn't have say * operator defined. You need to do something on top of it.
Additionally, zfc itself looks like loosely formalized say in wikipedia (and I am not sure if there is any strict formalization anywhere), we take it as common sense that it can utilize some simple logical rules (e.g. modus ponens), but what are exactly rules, which could be separate topic of research, this detail is skipped.
Eh? Any first course in set theory will present ZFC as a one-sorted theory with ten axioms (/schemas) in first order logic (inheriting an equality symbol, forall, implies etc) with one binary predicate (namely set membership), or will present a theory that is equiconsistent with a usual ZFC presentation. Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.
I referred to specific definition in wikipedia.
Your "first course notes" are irrelevant here, they can't be reviewed, they not proofread and unlikely can be considered as any reasonable quality if we are talking about real formalization of math.
I don't understand the point of your question. The "problem" of an ex-employee consciously or subconsciously bringing his learned experiences at your company to a competitor is literally the reason why non-competes exist. In fact, this topic is quite old.
My real point is this: if you're not allowed to bring your experiences with you, then the company exists to extract your creative thinking and skills. You can argue that's a fair trade for money. I don't necessarily disagree. But I think most of us find joy in learning, in building our own skills, in being able to reapply them elsewhere. And before LLMs and agents, I couldn't lose those skills and experiences no matter where I worked. As we progress, though, we've hit a point where we have to ask ourselves: at what price are we willing to trade complete ownership of our thinking and experiences for money?
>Suppose your function doodle_widget is supposed to take a Gonzo Widget, but you're worried somebody might call it with a Non-Gonzo Widget and that can't work.
No. Bjarne's C++ 20 Concepts are basically duck typing, you can express that you want a type where we can call the "is_gonzo" function but you can't say that you only want values of that type in which it's true.
Obviously you could re-design the software to follow a Rust-style type-state paradigm, have a NonGonzoWidget and GonzoWidget type which both inherit from Widget and now you can have your function take a GonzoWidget - but that's not what my comparison was about and this technique while possible is less common in C++
Edited to add: Actually, I should clarify that concepts have an idea called "modelling" and you can model anything you want, but the problem is that the machine doesn't care. So you can have a concept which models strings being about how awesome Donald Trump is, and the compiler won't and can't check that, but now a C++ program with a string matching that concept and the value "Trump is a moron" is an invalid C++ program, still compiles, still probably works, but your concept wasn't "modelled" so the program was not valid for whatever that's worth....
Yes, these types of scenarios are commonly handled with C++20 concepts. The main thing contracts do is provide a standardized scaffolding for enforcement.
Because that requires breaking the almost assured stipulation in a software license agreement that says "You will not try to RE this software", which is fine to ignore for home gamers, but not something you generally want to mess around with in a business setting where the risks are much higher.
The thing about this type of thinking is that it often requires risking millions of dollars and a major distraction from your primary goal in order to find out if it's true or not.
As would be running critical software certified for Windows on ReactOS as envisioned by GP. So, either we talk about an enterprise setting, in which GP already fucked up, or a more personal setting, in which both whaat GP and I said are reasonable
Also, the one thing that's important above all else in industrial automation is reliability. If your LLM doesn't know about one tiny little detail that ends up causing your product to fail, your customers start losing money and you can no longer point the finger at your PLC manufacturer. Make bad gambles like that and you won't be in business for long.
The reason industrial PLCs cost so much is because of their reliability. They need to be working flawlessly 50 years in the future. Trying to vibe code your way into a PLC compiler feels like it could blow up in your face after a little while.
That is also ignoring the safety PLCs with safety instructions that are certified for use with ISO 13849. Can you imagine getting inspected because your safety subsystem cause injury and you explain how you don't use the officially licensed software to program it.
You completely stripped what I said from its context. GP explicitely said they donate to ReactOS in the hopes of one day being able to run that industrial software on it instead of on Windows. In this context, running the software on ReactOS instead of official Windows would already fail your hypothetical inspections. This is why I suggested trying the LLM route.
If I had to explain a failure in production I would much rather say "due to availability of old hardware, we ran this on a different version of Windows/inside a VM/inside a Windows compatibility layer/Wine/ReactOS" than "we vibecoded the entire driver stack from scratch, go ask Claude why the plant blew up lol".
Running the same software in a different environment is unlikely to cause issues. But with vibe coding, you're throwing away the code the manufacturer certified as working, and the best possible outcome is it bricks your hardware in dev before things escalate to a post-mortem.
That is only recently become an option you could try, and we don't know long term how well it will work. Remember laws may change (and there are some legal issues around LLMs that are not clear at all)
reply