Posted by johnbender 10 hours ago
Couldn’t it very well be that you proved something that wasn't actually your program?
You can go a step farther and model the instruction set and architecture, and which point you can make proofs about the final binary directly (thereby sidestepping the problem of compiler bugs). At this point, your assumption is just that your physical hardware actually matches your model.
Correct. It can happen, where the actual code, could diverge from a lean representation of it, in a glaring or subtle way.
For things like programming languages we often have tedious, but slow, semantics that can be directly implemented in a suitable language. Then really all that a compiler or interpreter is is a faster version of those semantics.
If you are able to show correspondence between the fast and the the correct version, then you can toss the correct and slow version without even ever running it and just defer to the provably correct fast version.
Most software is ultimately like this
You can do it backwards. You declare the properties you want the resulting program/function to have, using a proof assistant like Lean, then prove that a program exists that meets those requirements, and the proof assistant spits two things: a confirmation that the proof is valid, and a piece of code that implements the proof, in the form of computer code.
At least that's how the proof assistant Coq would often be used. You still have the challenge of ensuring that you have defined the properties you really want in the first place, but at least it solves the part where you want the code to meet the specification.
Imagine having a formal spec for reality!
If I recall correctly the only news they used to post were new models updates, while now they have expanded their topics, or so I feel.
"What TLA+ can and can't check" https://news.ycombinator.com/item?id=49909056
"The internet discovers TLA+. Now what?" https://news.ycombinator.com/item?id=49863600
2017: Leslie Lamport: Video course on TLA+ (328 points, 74 comments) https://news.ycombinator.com/item?id=13918648 (219 points, 2018, 17 comments) https://news.ycombinator.com/item?id=16956778
2017: Writing correct lock-free and distributed stateful systems in Rust, with TLA+ (374 points, 94 comments) https://news.ycombinator.com/item?id=14373359
2019: TLA+ model checking made symbolic (197 points, 51 comments) https://news.ycombinator.com/item?id=21662484
2019: Introduction to TLA+ Model Checking in the Command Line (176 points, 44 comments) https://news.ycombinator.com/item?id=18937214
2019: Learn TLA+ (387 points, 92 comments) https://news.ycombinator.com/item?id=19661329 (310 points, 2020, 58 comments) https://news.ycombinator.com/item?id=22393653 (254 points, 2022, 64 comments) https://news.ycombinator.com/item?id=33010645 (350 points, 2022, 75 comments) https://news.ycombinator.com/item?id=31952643
2020: Using TLA+ in the Real World to Understand a Glibc Bug (166 points, 76 comments) https://news.ycombinator.com/item?id=24958504
2026: Hunting a 16-year-old SQLite WAL bug with TLA+ (239 points, 29 comments) https://news.ycombinator.com/item?id=48730953
...
https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
Did they solve Halting Problem?
OpenAI wrote some lean that pass the validate, write a math paper that feel plausible, but the paper don't match what's in lean.
Anthropic is now translating programs into Rocq proof. The same can happen.
Don't get me wrong -- this process can help catch some bug. but this is far from a proof
Nothing solidified Sharpee more than “compiling” this manual chapter by chapter.
But even that left gaps. I then designed a true DSL called Chord that compiles to Sharpee and this really ramped up the solidity of Sharpee.
no idea what you are even talking about
They're often simpler, and whole classes of security vulnerabilities are mitigated by design. My favorite example is SQL injection mitigated by having proper access controls in the DB. Why prove about every SQL statement that it cannot be nefarious, when we can just prove it about the connecting user? The user access carries the intent of what the application program wants to do with the database, in a separate channel, independently of the complexity of the application.