Is there a demonstration on practical proofs? #331
-
|
I've seen proves on natural numbers and boolean algebra, cool. But how useful is that for a real world use case? For example, if I have some function that queries the database via SQL, how hard is it to prove that it's impossible to SQL inject? I think such cases are really valuable, o.w. I don't find theorems useful for real world use cases. |
Beta Was this translation helpful? Give feedback.
Replies: 1 comment
-
|
We have a proof about the RLP encoding-decoding identity[1]. It turn's out, on the current version of Kind, those big proofs are kinda ugly (with a particularly big 1500 width line 😅 on this one). But they'll will be much more ergonomic on the upcoming version 2 of Kind. [1] |
Beta Was this translation helpful? Give feedback.
We have a proof about the RLP encoding-decoding identity[1]. It turn's out, on the current version of Kind, those big proofs are kinda ugly (with a particularly big 1500 width line 😅 on this one). But they'll will be much more ergonomic on the upcoming version 2 of Kind.
[1]
http://old.kindelia.org/App.RLP
https://github.com/Kindelia/Kind/blob/master/base/Ether/RLP/encode_identity.kind
https://github.com/Kindelia/Kind/blob/master/base/Ether/RLP/encode_identity/many.kind