3 ms·

The paper shows its age. A lot has happened since 1979. Projects like CompCert, seL4, Project Everest, Coq, Dafny, F* etc. shows what can be done with modern pr

The paper shows its age. A lot has happened since 1979. Projects like CompCert, seL4, Project Everest, Coq, Dafny, F* etc. shows what can be done with modern proof tools. And it is getting better every day. And I will claim that “formal” proofs, as practiced today by most professional mathematicians, are basically just informal proofs with more details, reviewed by flawed humans in a social process. Nothing wrong with that of course! But just pointing out that it doesn’t reach the high level of confidence that modern proof tools can deliver. The LEAN/mathlib project is an interesting example of what the future of truly formal mathematics might look like.

bmitc 3y ago
But "formal" proofs by proof systems are no less social processes. They are still developed by humans, require human agreement, and still have bugs. I think the main "bug" in proof systems is thinking that they will or should replace humans, as in most tech development today, rather than supplementing human activity.
- deterministic 3y ago
  Nope. With proof systems you have to convince the software. With traditional mathematics you have to convince a group of peers. Unless of course you consider interacting with software to be “social”.
  - bmitc 3y ago
    I didn't say it was the same social social process but still a social process. Software is written by humans. Proof systems are not impervious to mistakes or issues. The point is that it is just another way to help augment normal proofs. The writers of the proof systems need to convince themselves and others that they have imolemented and tested things properly. Someone writing a proof in such a system needs to convince others that they have translated the proof correctly and used the system appropriately. For example, the below article describes a very social process to writing down a Lean proof of a theorem: https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ https://www.quantamagazine.org/lean-computer-program-confirm... > Unless of course you consider interacting with software to be “social”. Yes, but not in the way you imply. When you write software, you are writing for other humans and thus communicating to other humans. The fact that a computer can perform a task based upon what's written is basically just the cherry on top and not the whole cake.
    - deterministic 3y ago
      Fields Medalist Peter Scholze does not agree with you: https://www.microsoft.com/en-us/research/project/lean/ https://www.microsoft.com/en-us/research/project/lean/ “Lean has already demonstrated its potential to revolutionise and radically accelerate mathematics, for example, helping Fields Medalist Peter Scholze confirm a new theorem in the Liquid Tensor Experiment.”

bmitc 3y ago

But "formal" proofs by proof systems are no less social processes. They are still developed by humans, require human agreement, and still have bugs. I think the main "bug" in proof systems is thinking that they will or should replace humans, as in most tech development today, rather than supplementing human activity.

deterministic 3y ago
Nope. With proof systems you have to convince the software. With traditional mathematics you have to convince a group of peers. Unless of course you consider interacting with software to be “social”.
- bmitc 3y ago
  I didn't say it was the same social social process but still a social process. Software is written by humans. Proof systems are not impervious to mistakes or issues. The point is that it is just another way to help augment normal proofs. The writers of the proof systems need to convince themselves and others that they have imolemented and tested things properly. Someone writing a proof in such a system needs to convince others that they have translated the proof correctly and used the system appropriately. For example, the below article describes a very social process to writing down a Lean proof of a theorem: https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ https://www.quantamagazine.org/lean-computer-program-confirm... > Unless of course you consider interacting with software to be “social”. Yes, but not in the way you imply. When you write software, you are writing for other humans and thus communicating to other humans. The fact that a computer can perform a task based upon what's written is basically just the cherry on top and not the whole cake.
  - deterministic 3y ago
    Fields Medalist Peter Scholze does not agree with you: https://www.microsoft.com/en-us/research/project/lean/ https://www.microsoft.com/en-us/research/project/lean/ “Lean has already demonstrated its potential to revolutionise and radically accelerate mathematics, for example, helping Fields Medalist Peter Scholze confirm a new theorem in the Liquid Tensor Experiment.”