Saturday, January 10, 2015

Does and explanation or an experiment qualify as a formal proof?

The short answer is no. Read on.
 
A formal proof is a sequence of sentences, starting from axioms, and developing using rules of inferences. Details are here: http://en.wikipedia.org/wiki/Formal_proof .
An experiment is not a formal proof. A formal proof is deductive while an experiment is inductive. Deduction is the method of inference in formal, rigorous models, such as math, computer science, and logic. While induction is the method of inference in observation-based models, such physics, biology, and chimestry (and similar fields). Induction cannot give useful and trustworthy information except if quantified correctly. The usual method of quantifying induction is through statistics (and more recently, machine learning). Experiments are mostly used in applied fields, where it suffices (and is possible) to show that something occurs. However, it is impossible to use experiments to show that something does not occur. In particular, it is impossible to show, using experiments, that a system is secure; since it is equivalent to showing that something bad does not occur.

Explanations are something different. Explanations are just a theory. Some of them may be tested, if they were falsifiable (testable, if you wish). But to the uninitiated, they can be very deceiving. Just because you can explain something, does not mean you proved it. An explanation just shows that something is plausible. But does not show that it is unavoidable. There is a cognitive bias known as confirmation bias (look it up) that say we are more likely to believe things that we can explain; which leads to serious logical fallacies. Therefore, a true scientist (going through masters and PhD) is trained to challenge his believes by trying to prove their opposite. Which is why in statistics we are usually interested in the null hypothesis instead of what we are actually trying to show. However, this is still more related to the inductive branch of inference, not the deductive branch.
In computer science, and in particular security and cryptography, deduction is the only way to show that we have an interesting result. This is why a formal proof is need, and why an explanation or an experiment is not. This is more serious that you can imagine; understanding this distinction is what makes a true scientist from a layperson.

Sunday, May 26, 2013

Quote



( The INEXACT flag mandated by IEEE Standard 754 for Binary Floating–Point Arithmetic would, if MATLAB granted us access to that flag, help us discriminate between solutions x that are exactly right and those, perhaps arbitrarily wrong, whose residuals vanish by accident.) - http://www.eecs.berkeley.edu/~wkahan/ieee754status/baleful.pdf

Useful commands



leaks
heap
fs_usage
lsof
vm_stat
netstat
tcpdump
sc_usage
otool
xxd
pbcopy
pdfgrep
du -sh /private/var/vm/sleepimage

Friday, May 3, 2013

Not having to specify DYLD_LIBRARY_PATH for your app when using Intel TBB (on Darwin/Mac OS X)

When using Intel Threading Building Blocks,  you have to link against their dynamic library. They do not provide a way for static linking, because when dynamic linking is used, their library has a shared state and they use that to prevent contention from over-threading.

However, the only way they provide to load their library at run-time is by having to provide a path to their library (libtbb.dylib) through the
DYLD_LIBRARY_PATH environment variable. Before your application launches you are going to have to set it in the shell. They provide a handy script to do it for you too. It may be inconvenient but it is doable (especially in non-production environments like scientific experiments).

However, although Valgrind is able to load their library correctly (and therefore run your program), GDB (7.5) can not do it. I am not able to debug my program because GDB says it can not load libtbb and dies.

So I used my Google-fu and found a solution. Just run the following command in the tbb/lib directory:

$ install_name_tool -id /absolute/path/to/libtbb.dylib libtbb.dylib


There you go. The difference is that without doing it, LD linker only puts the library name in the binary. I.e., otool -L shows only libtbb.dylib, no path, no nothing. After the command, LD puts the absolute path, and therefore it gets encoded in the binary; no need for DYLD_LIBRARY_PATH again.

I found the useful information at https://dev.lsstcorp.org/trac/wiki/LinkingDarwin.