3 ms·
Another interesting idea I've read, I think in a Haskell context, is proofs attached to values. You prove that a string originating from the user was HTML esca
by 323 4y ago
Another interesting idea I've read, I think in a Haskell context, is proofs attached to values.
You prove that a string originating from the user was HTML escaped - by calling the HTMLEscape function which attaches the proof - and then later in the code whenever you output it in the template it won't be escaped anymore because it's proven to be escaped.
- throwaway545232 4y agoI went down this rabbit hole 2 months ago and stumbled upon the Curry-Howard correspondence [1]. I don't understand why I find this stuff fascinating. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- CrazyPyroLinux 4y agoTLA+ [1] and Idris come to mind. Also Clojure Spec [2] For the specific case you mention, "taint analysis" would be appropriate. [1] https://softwareengineeringdaily.com/2018/11/09/tla-with-leslie-lamport/ https://softwareengineeringdaily.com/2018/11/09/tla-with-les... [2] https://www.youtube.com/watch?v=oyLBGkS5ICk https://www.youtube.com/watch?v=oyLBGkS5ICk Edit: links
- bvoq 4y agoTo add to this, you cannot have dependent proofs 'easily' in Haskell, but you can use LiquidHaskell for proofs!