Home » forums » LtU Forum

Functor

Functor Group AB, with its subsidiaries Functor AB and Functor Consulting AB, is a spin-off company, founded in early 2011, from Uppsala University, KTH, Stockholm University, University of Cambridge and Oxford University. Functor offers a new combined static analysis and hybrid testing tool and method (over 50% of bugs in C code can prevented) and a meta language modelling tool for domain engineering and DSL programming. Functor unleashes the next programming paradigm (STEW 2012) with zero learning curve.

Anyone know what this company is about? I see two products, Prevent and Scalor, some mentioning of C, Ocaml, Haskell, LLVM. But little detail.

Note: You can run one of their tools, Prevent, on a github project.

By marco at 2015-07-23 23:45 | LtU Forum | previous forum topic | next forum topic | other blogs | 3946 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Interesting

Sounds interesting. A lot of big claims there. But you're right, it's a bit thin on details. Although apparently "dependent types" are a core part of their technology. I was hoping that the R&D section would have more information on that, but there's not much there. I haven't got around to searching out publications from the founders or "associated researchers" yet.

I'll be impressed if they can pull off all that they claim with "zero learning curve".

By Allan McInnes at Fri, 2015-07-24 14:52 | login or register to post comments

Mbeddr-ish

In some ways their approach sounds similar to mbeddr: a set of domain-specific DSLs layered on top of C, integrated with tools for various kinds of analysis and static checking.

By Allan McInnes at Fri, 2015-07-24 20:41 | login or register to post comments

If I get it correctly: Type Theory

It seems to be based on type theory and rumor has it Martin-Low is on the board.

I guess that gives some insight into the approach they have taken, but the 'fundamental problems' probably don't change with the formalism you choose to base a static checker upon.

Where fundamental problems are a) C is a lousy language to reason abstractly about and b), except for trivial properties, it is hard to reason over programs.

The good thing about basing static checks on an elaborate type theory is of course, you can rely on full higher-order specifications and checks, for better or worse.

I don't see it scale either and it's a pity it does C instead of C++.

By marco at Sun, 2015-07-26 14:28 | login or register to post comments

You get correctly

Yes, type theory & dependent types seems the key. Of the affiliated researchers, at least Ghani & Altenkirch work on type-theory.

I've skimmed their "published paper" (http://www.functor.se/research/paradigm/), but it looks rather thin on details, and it doesn't seem published at a real conference.

Reasoning about C is harder, but people have managed. I'm mostly aware of approaches not using type theory, but abstract interpretation or separation logic. The following looks rather practical (maybe worth a separate discussion/front page item?), but I have just looked at the abstract:
https://dl.acm.org/citation.cfm?id=2594325

By Blaisorblade at Mon, 2015-07-27 09:23 | login or register to post comments