Lambda the Ultimate

Interpreting the Data: Parallel Analysis with Sawzall

"The query language, Sawzall, operates at about the level of a type-safe scripting language. For
problems that can be solved in Sawzall, the resulting code is much simpler and shorter – by a
factor of ten or more – than the corresponding C++ code in MapReduce."

Amber: "Amber for Parrot is a scripting language for the » Parrot virtual machine. It combines the traditional advantages of scripting languages with support for software correctness and large-scale software engineering."

It's described in self-deprecating terms, but it's interesting in several ways:

• Built in Eiffel and inspired by Eiffel
• Targeting the Parrot VM instead of Java's
• Implements "contract hardening" which sounds intriguing
• Not just another functional programming language, of which there are so many...
• I heard about it before LtU did

Ken Meltsner

Since DSL (Domain Specific Language) is almost an everyday topic for many programmers, I wonder how should a working programmer proceed to define and acturally use a formal semantics for her DSL? I do not mean a group of equations in LaTeX, but an effective method to help to reason about the programs within reasonable constraints for common projects. (Or, is there even bigger advantage to be taken?) To be specific, I was wondering if coq and isabelle and nusmv alike are usable for common projects? Is the cost (exclude the cost of learning) too high? And why? Thank you!