3 ms·

hey, I like your work on Paranoid Scientist. I've never come across hyper-properties: is this something you invented? Regarding hyper-properties: I assume they

by odipar 5y ago

hey, I like your work on Paranoid Scientist. I've never come across hyper-properties: is this something you invented? Regarding hyper-properties: I assume they only work on immutable data values, otherwise it would be hard to manage historical objects so that they can be part of any of the predicates. I'm working on a similar project that you may find interesting: https://odipar.github.io/manikin/ https://odipar.github.io/manikin/. I may want to include hyper-properties in future releases. edit: found this on hyperproperties: https://lamport.azurewebsites.net/pubs/hyper2.pdf https://lamport.azurewebsites.net/pubs/hyper2.pdf

trombonechamp 5y ago
Glad you like Paranoid Scientist, and thanks for the link to your project! Yes, you're right that it only works on immutable data types. At first I had implemented something which copies the object, but this used way too much ram and ended up being quite buggy with a lot of edge cases. I didn't invent the term hyperproperties (sadly). If you do end up implementing hyperproperties in runtime checks, you'll definitely want to look into to doing a statistical approach. The key to making this work is reservoir sampling (https://en.wikipedia.org/wiki/Reservoir_sampling https://en.wikipedia.org/wiki/Reservoir_sampling) - there are some more details of how I did this in the Paranoid Scientist paper (https://arxiv.org/abs/1909.00427 https://arxiv.org/abs/1909.00427).
still_grokking 5y ago
> https://lamport.azurewebsites.net/pubs/hyper2.pdf https://lamport.azurewebsites.net/pubs/hyper2.pdf What the parent post talks about is not even close what is described in that PDF above. "Proving" (or better verifying) stuff at runtime is trivial as it's only some asserts at the end. Analyzing the properties of programs before you run them is in an entire different league OTOH.

by odipar 5y ago

trombonechamp 5y ago

Glad you like Paranoid Scientist, and thanks for the link to your project! Yes, you're right that it only works on immutable data types. At first I had implemented something which copies the object, but this used way too much ram and ended up being quite buggy with a lot of edge cases. I didn't invent the term hyperproperties (sadly). If you do end up implementing hyperproperties in runtime checks, you'll definitely want to look into to doing a statistical approach. The key to making this work is reservoir sampling (https://en.wikipedia.org/wiki/Reservoir_sampling https://en.wikipedia.org/wiki/Reservoir_sampling) - there are some more details of how I did this in the Paranoid Scientist paper (https://arxiv.org/abs/1909.00427 https://arxiv.org/abs/1909.00427).

still_grokking 5y ago

> https://lamport.azurewebsites.net/pubs/hyper2.pdf https://lamport.azurewebsites.net/pubs/hyper2.pdf What the parent post talks about is not even close what is described in that PDF above. "Proving" (or better verifying) stuff at runtime is trivial as it's only some asserts at the end. Analyzing the properties of programs before you run them is in an entire different league OTOH.