3 ms·

I recall an experiment in proving software correct from the 1990s that found more errors in the final proof annotations than in the software it had proved corre

I recall an experiment in proving software correct from the 1990s that found more errors in the final proof annotations than in the software it had proved correct. Then, I foresee 2 other obstacles, 1 of which may disappear: 1. Actually knowing what the software is supposed to do is hard. Understanding what the users actually want to do and what the customers are paying to do --which aren't necessarily the same thing--is complex 2. The quality of the work of many software developers is abysmal and I don't know why they would be better at a truth language than they are at Java or some other language. Objection 2 may disappear to be replaced with AI systems with the attention to do what needs to be done. So perhaps things will change in that to make it worthwhile...

jsmorph 6mo ago
Re 1: Discussing and guiding the desirable theorems for general-purpose programs has been a major challenge for us. Proofs for their own sake (bad?) vs glorious general results (good but hard?). Actual human guidance there can be critical there at least for now.
gr_norm 6mo ago
Mind linking the experiment? Sounds interesting.
- deleted 6mo ago
  [deleted]
Groxx 6mo ago
I think the hope for 2 is that those programmers would be forced into inaction by the language safety, rather than being allowed to cause problems. I don't really think that works either, because there's endless ways to add complication even if you can't worsen behavior (assuming that's even possible). At best they might be caught eventually... but anyone who has worked in a large tech company knows at least a few people who are somehow still employed years later, despite constant ineptitude. Play The Game well enough and it's probably always possible.
- teiferer 6mo ago
  It's even conceivable that 2 gets worse with AI: The AI does the proof for them, very convolutedly so, and as long as the proof checker eats it, it goes through. Comes the day when the complexity goes beyond what the AI assistant can handle and it gives up. At that point, the proof codes complexity will for a long time have passed the threshold of being comprehensible for any human and there is no progress possible. Hard stop.
  - codebje 6mo ago
    Using a proof language with an SMT solver is basically that: an inexplicable tick that it’s fine, until a small change is needed, the tick is gone, and nothing can say why.
    - zozbot234 6mo ago
      That's basically what sledgehammer (mentioned in the article) boils down to. The Lean folks use some safeguards to avoid issues with that, such as only using their "grind" at the end of a proof, where all the "building blocks" have been added to context.
- sdeframond 6mo ago
  > I think the hope for 2 is that those programmers would be forced into inaction by the language safety, rather than being allowed to cause problems. Ah! That's funny :) In practice there are always ways to circumvent safety, especially when it is easier than the alternative. In a Typescript codebase I work on, I configured the type-checker to fordbid `any`. Should be easy enough to use `object` When we don't know the type, right? Well then things started being serialized into `string` way more often than I'd like...
  - Groxx 6mo ago
    tbh if you think a serialized string bypasses anything in a proof-oriented language... I think that just means you haven't used one before. stringly-typed code is no less safe than strict types in these systems, though it's generally quite a lot more work: more things are fallible, and you need to repeatedly re-build or check every guarantee you are still requiring in other code that you interact with. the exception is if you explicitly state X is a true statement, as many have some kind of bypass like that (an axiom or assumption or whatever). you could build a system that uses this everywhere to break most of the rules, like you can use `any` everywhere, but it'll be extremely obvious if that's the case.
deterministic 6mo ago
Check out SeL4 (a proven correct micro kernel used by billions of devices worldwide) and CompCert (a proven correct C compiler used by Airbus).

jsmorph 6mo ago

Re 1: Discussing and guiding the desirable theorems for general-purpose programs has been a major challenge for us. Proofs for their own sake (bad?) vs glorious general results (good but hard?). Actual human guidance there can be critical there at least for now.

gr_norm 6mo ago

Mind linking the experiment? Sounds interesting.

deleted 6mo ago
[deleted]

Groxx 6mo ago

I think the hope for 2 is that those programmers would be forced into inaction by the language safety, rather than being allowed to cause problems. I don't really think that works either, because there's endless ways to add complication even if you can't worsen behavior (assuming that's even possible). At best they might be caught eventually... but anyone who has worked in a large tech company knows at least a few people who are somehow still employed years later, despite constant ineptitude. Play The Game well enough and it's probably always possible.

teiferer 6mo ago
It's even conceivable that 2 gets worse with AI: The AI does the proof for them, very convolutedly so, and as long as the proof checker eats it, it goes through. Comes the day when the complexity goes beyond what the AI assistant can handle and it gives up. At that point, the proof codes complexity will for a long time have passed the threshold of being comprehensible for any human and there is no progress possible. Hard stop.
- codebje 6mo ago
  Using a proof language with an SMT solver is basically that: an inexplicable tick that it’s fine, until a small change is needed, the tick is gone, and nothing can say why.
  - zozbot234 6mo ago
    That's basically what sledgehammer (mentioned in the article) boils down to. The Lean folks use some safeguards to avoid issues with that, such as only using their "grind" at the end of a proof, where all the "building blocks" have been added to context.
sdeframond 6mo ago
> I think the hope for 2 is that those programmers would be forced into inaction by the language safety, rather than being allowed to cause problems. Ah! That's funny :) In practice there are always ways to circumvent safety, especially when it is easier than the alternative. In a Typescript codebase I work on, I configured the type-checker to fordbid `any`. Should be easy enough to use `object` When we don't know the type, right? Well then things started being serialized into `string` way more often than I'd like...
- Groxx 6mo ago
  tbh if you think a serialized string bypasses anything in a proof-oriented language... I think that just means you haven't used one before. stringly-typed code is no less safe than strict types in these systems, though it's generally quite a lot more work: more things are fallible, and you need to repeatedly re-build or check every guarantee you are still requiring in other code that you interact with. the exception is if you explicitly state X is a true statement, as many have some kind of bypass like that (an axiom or assumption or whatever). you could build a system that uses this everywhere to break most of the rules, like you can use `any` everywhere, but it'll be extremely obvious if that's the case.

deterministic 6mo ago

Check out SeL4 (a proven correct micro kernel used by billions of devices worldwide) and CompCert (a proven correct C compiler used by Airbus).