You know, I'm not really into cryptocurrency, but it does seem like it's contributing to a resurgence of interest in formal methods. So - thank you, cryptocurrency community!
I find it funny that the reason we want the cryptocurrencies to be formally verified is because we want rock-solid financial transactions so that this distributed story is always accurate (which is good), but actual banks don't seem to have these same requirements.
NOTE: Could be wrong on that last point, getting my information about banks third-hand, it's possible that banks are using formal verification. Can someone who works at a bank confirm?
I totally understand why blockchain isn't the standard for everything right now; my statement was in regards to formal methods to ensure correctness. For example, "reversing" a transaction could totally be modeled in TLA+ (and probably other systems, I'm just most familiar with TLA+ than most other systems), which would provide model checking (and possibly even proofs) that you would not otherwise have.
https://www.merriam-webster.com/dictionary/fait%20accompli
There's probably a better term but English isn't my first language.
It seems to me that having every bit of evidence on their end to prove that they are guaranteeing our transactions would be a really good thing....I suppose this solution might just work itself out if banks actually start relying on some kind blockchain to secure their transactions.
Its cheaper for everyone for them to say oops and give you the money back.
Its more expensive for you to sue than for them to be sued.
In fact you would immediately seek another job if you came from formal methods practice and then saw production code at just about any of the different animals called banks.
> [Coq, VST, CompCert]
> Formal methods: https://en.wikipedia.org/wiki/Formal_methods
> Formal specification: https://en.wikipedia.org/wiki/Formal_specification
> Implementation of formal specification: https://en.wikipedia.org/wiki/Anti-pattern#Software_engineer...
> Formal verification: https://en.wikipedia.org/wiki/Formal_verification
> From "Why Don't People Use Formal Methods?" https://news.ycombinator.com/item?id=18965964 :
>> Which universities teach formal methods?
>> - q=formal+verification https://www.class-central.com/search?q=formal+verification
>> - q=formal+methods https://www.class-central.com/search?q=formal+methods
>> Is formal verification a required course or curriculum competency for any Computer Science or Software Engineering / Computer Engineering degree programs?
https://www.absint.com/compcert/structure.htm
A problem with both seL4 and CompCert is that the code written to express the proofs is huge, much larger than code that actually does stuff. This puts a ceiling on the size of the projects we can verify.
F* is a language that tries to address that, by finding proofs with z3, a smt prover; z3 can't prove everything on its own but it cuts down proof code by orders of magnitude. They have written a verified cryptography stack and TLS stack, and want to write a whole verified http stack.
https://github.com/project-everest/hacl-star
https://project-everest.github.io/
F* (through Low, a verified low-level subset of F) can extract verified code to C, which is kind of the inverse than the seL4 proof: seL4 begins with C code and enriches it with proofs of correctness; hacl* (a verified crypto F* lib) begins with a proven correct F* code and extracts C code (I gather the actual crypto primitives is compiled directly to asm code because C has some problems with constant time stuff). This enables hacl* to make bindings to other languages that can just call C code, like this Rust binding
https://github.com/franziskuskiefer/evercrypt-rust
Also this F* stuff is all free software / open source, so it might become a very prevalent crypto and TLS stack
That said, TLA+ is written separately from the code. There could of course be bugs in the translation of TLA+ -> C...TLA+ is about checking the design itself, not the code.
I'm curious which static analysis tool you were using. I used to work in SPARK Ada and false positives were not really a thing due to how it worked. But I've heard of others that were much less restrictive which ended up with lots of false positives, or "maybe" cases that then wasted everyone's time. I can see how systems like that would put people right off using them.
See: Use of Formal Methods at Amazon Web Services
https://lamport.azurewebsites.net/tla/formal-methods-amazon....
> Proof-carrying data (PCD) enables a set of parties to carry out an indefinitely long distributed computation where every step along the way is accompanied by a proof of correctness. It generalizes incrementally verifiable computation
This has the potential to remove the element of trust that you currently must place in the provider of computation resources. With SNARKs you can simply ask them to include a proof that they actually performed the computation that is sublinear in the length of the proof and sublinear in the amount of time taken to verify the proof.
Of course this will always be more computationally expensive for the provider of the computation resources to both do the work and provide the proof.