> What is the difference between "verifying" the
> correctness of code, as they say here, vs "proving"
> the correctness of code, as I sometimes see said
> elsewhere?
There is not much difference, except that verification usually includes identifying a formal logical proposition about the behaviour of the code.
In other words, formally verified code is code that has been proven to meet at least one formal proposition about its behaviour - for example, a proposition about a function f might be: if variable x is greater than 0, then `f(x) = 1`.
There is no such thing as proving something 'correct', you need someone to define what exactly correct means, and then someone proves it meets that definition. So the proving is only a subset of the overall formal verification task.
> Also, is there a good learning resource on "proving" things about code for working
> programmers without a strong CS / math background?
If you want to get into specifics, you might need to pick an approach. You could learn a dependently typed language, for example there are some good resources out there on proving things in Agda or Idris. Or perhaps play around with one of the formal verification systems that can be bolted on to C or Rust.
> Edit: I'm also very curious why "zero knowledge" proofs are so significant, and why this
> is so relevant. Eg I heard people talking about this and don't really understand why it's
> so cool: x.com/ZorpZK
ZK is an exciting area of cryptology because breakthroughs in that area power new applications that people wouldn't have thought possible before. Applications to cryptocurrencies in particular can solve some of their scaling and privacy problems.
For example, one of the biggest problems with cryptocurrencies is that every single transaction ever needs to be recorded in a ledger that is distributed to every node participating in the network. That simply won't scale to microtransactions. Let's say that 1000 people each start with 1 coin, and do 100,000 small transactions averaging 0.001 coins amongst themselves (maybe they bought a coffee, or paid for information on a per-view basis, or whatever). Storing those 100,000 transactions forever will have an ongoing cost for every one of thousands of nodes on the network long after the transaction has happened.
Now that could be solved with centralisation - the parties send their transactions to a trusted company, who maintains balances for each of them without sending transactions to the network, but lets them withdraw their balance to the network if they ever want to. But centralisation is a risk - what if the company betrays their trust?
Zero-knowledge cryptography allows for the parties to roll up the signed transactions into a cryptographic proof saying, given these were the balances at the start of the 100,000 transactions, the person creating the roll-up has access to the signed transactions proving that the balances of each of the 1,000 parties at the end are this. Notably, the proof can be much smaller than the size of the 100,000 transactions. So that enables applications where people work off in 'side chains', and but can merge the side chain back into the main chain by submitting proof about the effects (but not all the detail of) the side chain into the main chain.
There is not much difference, except that verification usually includes identifying a formal logical proposition about the behaviour of the code.
In other words, formally verified code is code that has been proven to meet at least one formal proposition about its behaviour - for example, a proposition about a function f might be: if variable x is greater than 0, then `f(x) = 1`.
There is no such thing as proving something 'correct', you need someone to define what exactly correct means, and then someone proves it meets that definition. So the proving is only a subset of the overall formal verification task.
> Also, is there a good learning resource on "proving" things about code for working > programmers without a strong CS / math background?
Most will be specific to a particular technology and type of verification. There are some courses online that provide a high level overview, e.g. https://anton-trunov.github.io/csclub-coq-course-spring-2021....
If you want to get into specifics, you might need to pick an approach. You could learn a dependently typed language, for example there are some good resources out there on proving things in Agda or Idris. Or perhaps play around with one of the formal verification systems that can be bolted on to C or Rust.
> Edit: I'm also very curious why "zero knowledge" proofs are so significant, and why this > is so relevant. Eg I heard people talking about this and don't really understand why it's > so cool: x.com/ZorpZK
ZK is an exciting area of cryptology because breakthroughs in that area power new applications that people wouldn't have thought possible before. Applications to cryptocurrencies in particular can solve some of their scaling and privacy problems.
For example, one of the biggest problems with cryptocurrencies is that every single transaction ever needs to be recorded in a ledger that is distributed to every node participating in the network. That simply won't scale to microtransactions. Let's say that 1000 people each start with 1 coin, and do 100,000 small transactions averaging 0.001 coins amongst themselves (maybe they bought a coffee, or paid for information on a per-view basis, or whatever). Storing those 100,000 transactions forever will have an ongoing cost for every one of thousands of nodes on the network long after the transaction has happened.
Now that could be solved with centralisation - the parties send their transactions to a trusted company, who maintains balances for each of them without sending transactions to the network, but lets them withdraw their balance to the network if they ever want to. But centralisation is a risk - what if the company betrays their trust?
Zero-knowledge cryptography allows for the parties to roll up the signed transactions into a cryptographic proof saying, given these were the balances at the start of the 100,000 transactions, the person creating the roll-up has access to the signed transactions proving that the balances of each of the 1,000 parties at the end are this. Notably, the proof can be much smaller than the size of the 100,000 transactions. So that enables applications where people work off in 'side chains', and but can merge the side chain back into the main chain by submitting proof about the effects (but not all the detail of) the side chain into the main chain.