Cedar used to be written in Dafny, but AWS abandoned that implementation and rewrote it in Lean. https://aws.amazon.com/blogs/opensource/lean-into-verified-s...
> I looked a little into RustBelt; how would it have helped this `Pin` issue? I browsed [1] a bit and it seems like `Pin` would have to have been proven on its own in an ad-hoc way not covered by RustBelt. To clarify,…
I might be mistaken, but my understanding is that it does not. You still need to trust the implementation of the logic. But if you don't trust that, you wouldn't trust the compiler correctness proof anyway, so…
CompCert doesn't do this, but CakeML, a verified compiler for a variant of ML bootstraps itself in the logic: > A unique feature of the CakeML compiler is that it is bootstrapped “in the logic” – essentially, an…
> Are you including Bitcoin script when you say consensus? Currently, no. Our model considers "consensus" to be agreement on the ordering of transactions. We don't yet interpret the transactions. However, agreement on…
I agree, and there are efforts to develop formally verified implementations of Nakamoto consensus (which I'm involved in). We've published a paper a year ago about our efforts and first results and I'm currently…
> I’d really appreciate [...] links to the work of similar initiatives Take a look at Quorum, a "programming language which is designed to be accessible to individuals with disabilities and is widely used in schools for…
> SAT solvers generally have poor support for constructive logic, the kind of logic used in theorem provers based on dependent types like Coq. Arguably, this is no longer the case. FStar [1] has dependent types, monadic…
The link is that both these policies hurt US tech companies. With that lens, there is no inconsistency.
Apparently, v1.0 of the Facebook Graph API could access users' private messages via the 'read_mailbox' API request [1]. This was deprecated when v2.0 launched. "Version 1.0 of the Graph API launched on April 21, 2010.…
That sounds a lot like BitMessage. https://bitmessage.org/bitmessage.pdf
Cedar used to be written in Dafny, but AWS abandoned that implementation and rewrote it in Lean. https://aws.amazon.com/blogs/opensource/lean-into-verified-s...
> I looked a little into RustBelt; how would it have helped this `Pin` issue? I browsed [1] a bit and it seems like `Pin` would have to have been proven on its own in an ad-hoc way not covered by RustBelt. To clarify,…
I might be mistaken, but my understanding is that it does not. You still need to trust the implementation of the logic. But if you don't trust that, you wouldn't trust the compiler correctness proof anyway, so…
CompCert doesn't do this, but CakeML, a verified compiler for a variant of ML bootstraps itself in the logic: > A unique feature of the CakeML compiler is that it is bootstrapped “in the logic” – essentially, an…
> Are you including Bitcoin script when you say consensus? Currently, no. Our model considers "consensus" to be agreement on the ordering of transactions. We don't yet interpret the transactions. However, agreement on…
I agree, and there are efforts to develop formally verified implementations of Nakamoto consensus (which I'm involved in). We've published a paper a year ago about our efforts and first results and I'm currently…
> I’d really appreciate [...] links to the work of similar initiatives Take a look at Quorum, a "programming language which is designed to be accessible to individuals with disabilities and is widely used in schools for…
> SAT solvers generally have poor support for constructive logic, the kind of logic used in theorem provers based on dependent types like Coq. Arguably, this is no longer the case. FStar [1] has dependent types, monadic…
The link is that both these policies hurt US tech companies. With that lens, there is no inconsistency.
Apparently, v1.0 of the Facebook Graph API could access users' private messages via the 'read_mailbox' API request [1]. This was deprecated when v2.0 launched. "Version 1.0 of the Graph API launched on April 21, 2010.…
That sounds a lot like BitMessage. https://bitmessage.org/bitmessage.pdf