Transcript Haskell in an Industrial Context

Haskell in an Industrial Context
Andy Moran
Haskell, Galois, and the Future
• Galois’ use of Haskell: why and where
• Challenges in continuing to use Haskell
• How do we meet these challenges
– Some suggestions
Galois Summary
• Mission: Advanced technology development
for Information Assurance
• Expertise
– Crypto development and validation
– Multi-level and cross-domain security
– Secure middleware
• Capabilities
–
–
–
–
–
High assurance engineering
Abstract modeling & analysis
Application of relevant theoretical research
Rapid prototype development
Domain-specific language development
Corporate Background
• Founded in 1999; spun off from funded OGI
research
• Profitable last 8 quarters, >50% CAGR
• Funding
– Self-funded from revenues
– 90% employee owned
• 6 Active Projects
– Mix of research and product development
• Clients
– U.S govt, multiple primes
• 20 employees total
– 15 technical staff
– Additional contract employees and subcontractors
High Assurance Engineering
• High Assurance means:
– Formal and semi-formal specifications, designs, models
– Formal and semi-formal correspondence arguments
• Not necessarily mathematical proofs
– Traditional testing
– Many non-functional, non-technical requirements about:
•
•
•
•
Physical security of code
Software process documentation
Change management
Release management
• High Assurance is not complete formal verification
– Which is why we think we have a chance …
• It’s all about gathering evidence that the product does what it
should
– It’s not about proving that it always does
Galois and Haskell
• Galois’ focus is High Assurance development
• With two exceptions, every project we’ve ever done or are
now doing have uses Haskell
• We delivered tools that are being used heavily:
– Cryptol
– GUI debugger for a specialized chip
– Syntax extension tool for client’s own language (suped-up
Happy + OCaml P4)
• Our biggest project relies upon Haskell
– High assurance arguments predicated upon use of Haskell
• Another project is about Haskell
• All others benefit from using Haskell
Why Haskell: Technical Benefits
• Type system very strong, expressive
• Type system exposes effects
• Laziness encourages combinatorial design
– Natural for many problems, particularly compilers
• Haskell is very high-level
– Promotes design-level programming
• Haskell programs look like designs to non-practitioners
– Enables us to try out creative solutions that might not be
tractable with traditional languages
• Able to express more complex algorithms
• Design-level debugging
– Trivial bugs disallowed by type system
– Get straight to the real bugs
• We’re very familiar with Haskell
But these arguments do not a business case make!
The Big Win: High Assurance
• Haskell is close to its semantics
– Providing evidence for H.A. properties is
possible
– Haskell is amenable to formal techniques
• Haskell’s type system can express and enforce
desirable H.A. properties (such as data
separation)
• Good handle on H.A. correspondence
arguments:
– Specification, design, model: all in Haskell
Indirect Business Benefits
• High productivity:
– We can prototype products/tools very quickly
• Competition:
– Not many companies out there using Haskell as an
enabling technology
• Familiarity:
– Most of Galois has been using Haskell since day 1
• Possibilities:
– Allows greater scope for high assurance development
– We can build in more functionality, to higher assurance
• Quality of Staff:
– Haskell practitioners tend to be extremely bright
It’s Not All Beer and Skittles …
• There are problems with relying upon Haskell:
– Technical issues
– Support
– Long-term viability
– Customer needs
– Customer perception
– Staffing
– Special government client needs
Development Issues
• We’re surrounded by nails
– When all you’ve got is a hammer …
• Happily, it’s a Swiss Army hammer
• Debugging can be a pain
– Especially debugging in the IO monad
– Existing debuggers tend not to support language
extensions
• Libraries only scratch library writers itch
– Not designed with industrial applications in mind
• Haskell encourages “abstraction addiction”
– It’s very easy to get tied up in knots
– Too much abstraction leads to maintenance headaches
Support Issues
• Volunteer-based support for compiler only
– Can’t depend on getting that showstopper fixed in time to meet
your deadline
• We push GHC to its limits, and so expose problems in the RTS
• Without Sigbjørn Finne on the payroll, at least three of our projects
would have been held up indefinitely
– Threaded RTS, Asynchronous I/O for Windows, elusive GC bug
– No 24 hour hotline
– Only common platforms get any support
• No industrial-grade tool support
– Profilers limited; debuggers very limited
– Libraries not tuned for performance
– Libraries, language extensions documented mainly in research
papers, if at all
• GHC user manual gives reference-level documentation to extensions
– IDEs very limited
Long-Term Viability
• Reliant upon Simon and Simon
– What if they start working on Word 2006?
– Others starting to play larger role, but still
small handful of key players
• Still a research language
– Exists to be test bed for experiments:
• Language design (Template Haskell, exotic type
systems)
• Compiler implementation (eval-apply, CMM back-end)
– This is A Good Thing
• But we need a stable language too …
General Business Issues
• Customers see problems:
– How are they going to maintain the code we built for
them?
– Will this weird language even be around next year?
• Customer perception:
– “What’s Haskell?”
– “What’s Functional Programming?”
– “Functional programs are slow!”
– “Why is it better than Java?”
– “If it’s so great, why isn’t everyone using it?”
• Staffing:
– Not that many Haskell practitioners out there
– Currently, we also need U.S. citizens
Government Issues
• Pedigree of compiler source
– Corralled repository
– Who worked on it before corralling
• Security of compiler source
– Who has write access
– How is repository protected
• Physical (key card access to server room)
• Network
– How patches are vetted before being applied
• How many “trusted” eyes have reviewed compiler source?
• These questions are asked of any tool being used to develop
sensitive applications
– If tool source changes often, the burden is increased
– Especially if we also need to update formal arguments and
models each time there is a change
Are We Alone?
How Might We Solve These Problems
Together?
What’s Been Tried Before?
Why Didn’t It Work?
Haskell Consortium
• An affiliation of companies that use Haskell, together
funding
– Providing technical support for compilers and tools
•
•
•
•
•
Timely bug-fixes
Patch release management
Version, platform management
Keeping up with GHC patches
Evaluating GHC enhancements for inclusion
– Pursuing industrial-grade development
• Developing new tools
• Enhancing existing tools
• Developing experimental compilers, interpreters, runtime systems
• Funding could be augmented:
– Members’ clients? Government? Charity?