Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Open-sourcing Facebook Infer: Identify bugs before you ship

code.facebook.com

Post reply on HN
Print view View original

21–30 of 121 posts

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#21

Post by psuter »

tptacek wrote: post #19

Can someone explain-it-like-I'm-a-90s-programmer (ELi90s?) why so much symbolic evaluation stuff gets done in OCaml? What does OCaml do that makes it so well suited for this problem domain? (I know a very little bit about symbolic evaluation and have done a very very little bit of it).

Symbolic reasoning involves a lot of term-matching and term-rewriting. These tasks are best accomplished in programming languages that have first-class support for recursive terms (aka. algebraic data types). Popular candidates these days are OCaml, Haskell, Scala.

While I am not certain the premise holds (OCaml dominance), one possible explanation is that many programmers were introduced to ML/OCaml through the compiler construction course and Andrew Appel's book.

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#22

Post by istvan__ »

tptacek wrote: post #19

Can someone explain-it-like-I'm-a-90s-programmer (ELi90s?) why so much symbolic evaluation stuff gets done in OCaml? What does OCaml do that makes it so well suited for this problem domain? (I know a very little bit about symbolic evaluation and have done a very very little bit of it).

I think one part of this is the OCaml type system. It just seems to be very suitable for symbolic manipulations. You can do a lot with algebraic data types.

http://en.wikipedia.org/wiki/Algebraic_data_type

The other feature that I personally think is great in OCaml is pattern matching. This can help you expressing computation on symbols, where usually you have few options for the input. See following:

https://github.com/facebook/infer/blob/master/infer/src/chec...

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#23

Post by pcwalton »

tptacek wrote: post #19

Can someone explain-it-like-I'm-a-90s-programmer (ELi90s?) why so much symbolic evaluation stuff gets done in OCaml? What does OCaml do that makes it so well suited for this problem domain? (I know a very little bit about symbolic evaluation and have done a very very little bit of it).

In addition to what the other commenter said, pattern matching is really nice for this kind of thing. Of all of the functional programming languages, OCaml has probably the most sophisticated pattern matching engine around (and we basically copied it into Rust, incidentally), supporting or-patterns, multiple bindings, guards, and so forth. Pattern matching lets you essentially match on the shape of subtrees of arbitrary data structures with complex predicates.

If you're familiar with old-school compiler construction, this is like having a souped-up BURG built into the language. For example, pattern matching lets you say things like "if I have Load(Var, Add(Var, Constant)) where constant is a small power of two, fold it into the x86 indexed addressing mode" in one line. Unsurprisingly this is useful not only for compiler construction but for any kind of term rewriting/symbolic manipulation.

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#25

Post by crudbug »

aristus wrote: post #17
amirmc wrote: post #3

More OCaml code coming out of FB. Can add this to the list, which includes, Hack, Flow and Pfff [1]. The kinds of bugs it finds are listed at: http://fbinfer.com/docs/infer-bug-types.html It's interesting to see how building tools with languages like OCaml can reduce bugs for teams, without them having to change the language itself. I do wonder what things would be like if such languages we're used directly more wide…

Legend has it there is a small room at FBHQ, containing a quorum of OCaml committers, all of them French for some reason, hacking away at level of abstraction beyond the ken of mortal man.

I like this plot .. May be OCaml Movie :)

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#26

Post by aaggarwal »

istvan__ wrote: post #20

I am extremely happy to see Facebook using OCaml, it is good the get some more traction in that community. I hope it gains velocity over time and becomes a viable option especially for startups where there is no technical debt. It has amazing features and as you can see even very complex problems can be solved in a concise, terse way. Kudos to Facebook on this one.

As it is pointed out, OCaml has support for algebraic data types and symbolic evaluation, doesn't this make it an excellent language for natural language processing? Are there any more examples anyone is aware of?

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#27

Post by tptacek »

pcwalton wrote: post #23
tptacek wrote: post #19

Can someone explain-it-like-I'm-a-90s-programmer (ELi90s?) why so much symbolic evaluation stuff gets done in OCaml? What does OCaml do that makes it so well suited for this problem domain? (I know a very little bit about symbolic evaluation and have done a very very little bit of it).

In addition to what the other commenter said, pattern matching is really nice for this kind of thing. Of all of the functional programming languages, OCaml has probably the most sophisticated pattern matching engine around (and we basically copied it into Rust, incidentally), supporting or-patterns, multiple bindings, guards, and so forth. Pattern matching lets you essentially match on the shape of subtrees of arbitr…

Ok, tangent question: if I wanted an interesting project to learn Rust with, would a symbolic evaluation checker for (say) C code be a really good fit? In the same sense as emulators turned out to be a fantastic fit for Golang?

If that's true, what are the features of Rust that make this so, and roughly how would they apply to that problem domain? (I could answer that question for Golang and emulators pretty quickly).

(Hopefully this question comes across the way I intend it to, which is: I have no plans on using OCaml any time soon, believe the comments that say you want a language with pattern matching to do this in, and would love to tinker more with both Rust and symbolic evaluation.)

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#28

Post by sadert »

What's the difference between this and the Clang analyzer, which comes with Xcode already? I expected that comparison to be on the front page...

http://clang-analyzer.llvm.org/

(obviously it supports Java as well, but I assume Android Studio comes with some sort of static analyzer as well, so same question?)

It specifically calls out null pointer exceptions but those... aren't a thing... in Objective-C, messages passed to nil return all 0 bits, and that's okay (unless they mean null dereferences...).

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#29

Post by tptacek »

istvan__ wrote: post #22
tptacek wrote: post #19

Can someone explain-it-like-I'm-a-90s-programmer (ELi90s?) why so much symbolic evaluation stuff gets done in OCaml? What does OCaml do that makes it so well suited for this problem domain? (I know a very little bit about symbolic evaluation and have done a very very little bit of it).

I think one part of this is the OCaml type system. It just seems to be very suitable for symbolic manipulations. You can do a lot with algebraic data types. http://en.wikipedia.org/wiki/Algebraic_data_type The other feature that I personally think is great in OCaml is pattern matching. This can help you expressing computation on symbols, where usually you have few options for the input. See following: https://github.…

I can sort of make sense of this, but I don't know enough OCaml or FbInfer to really grok it. Why would this be a particularly good example of how OCaml simplifies symbolic evaluation?

Thank you, by the way! Actual code examples are kind of exactly what I'd like to see.

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#30

Post by suyash »

sadert wrote: post #28

What's the difference between this and the Clang analyzer, which comes with Xcode already? I expected that comparison to be on the front page... http://clang-analyzer.llvm.org/ (obviously it supports Java as well, but I assume Android Studio comes with some sort of static analyzer as well, so same question?) It specifically calls out null pointer exceptions but those... aren't a thing... in Objective-C, messages pass…

Yes Android Studio does come with a static checker called 'Lint' and I'm wondering the same. What are infer's advantages over 'Lint' or even 'findbugs'?
Post reply on HN