search

lawrencecpaulson / lawrencecpaulson.github.io

the blog "Machine Logic"
13 stars 0 forks source link

https://lawrencecpaulson.github.io/2022/01/05/LCF.html #6

Open utterances-bot opened 2 years ago

utterances-bot commented 2 years ago

Machine Logic

https://lawrencecpaulson.github.io/2022/01/05/LCF.html

phlegmaticprogrammer commented 2 years ago

I think you would want all three! Readable proofs, LCF, and de Bruijn, in that order of importance. That readable proofs have the highest priority is obvious, as it is the sole tool of mathematicians. That LCF is more important than de Bruijn is also clear: if your logic is simple enough, your proof objects are just a transaction log of the activities of your LCF kernel.

Managing the size of proof objects is just an engineering task, for example there is no reason why it should affect RAM usage much, it should be just SSD-bound if implemented properly. And of course, it doesn't even have to run always, but just on demand (for example before handing out that million pound reward for proving Fermat's Last Theorem in your system), and during nightly integration tests, to make sure that the proof object mechanism actually works reliably.

phlegmaticprogrammer commented 2 years ago

Furthermore, taking the security of a proof assistant seriously is important as soon as mathematical theories are traded in a market place. That might sound silly now, but in the end ALL of sufficiently advanced engineering is mathematics, so this will eventually happen. I also wonder what the emergence of such a market will do to the patent system (and the other way around).

lawrencecpaulson commented 2 years ago

How could I disagree? All those things are possible with Isabelle. And little of the formal material available today is readable unless it was done in Isabelle.