Lambda the Ultimate

In catching up with my Bloglines subscriptions, I came across the the following piece by Ivаr Jаcobson, Bertrаnd Mеyer, and Richаrd Solеy:

Given the ambition of the Semat project it would be surprising if it did not cause some controversy. Alistair Cockburn wrote a long critique. Martin Fowler echoes Cockburn and states that the effort is “fundamentally doomed”.

Scott Ambler thinks SEMAT is good. What does Dаniel Bеrry think?

Hello

I've been thinking recently about schema languages for data, and in particular what it takes to give them a formal foundation.

I expect a lot of type system theory would apply, since these are effectively type systems for data, however they're a bit different to a typical programming language's type system.

On the one hand they often include value-level constraints like 'integer between 0 and 16', which I imagine might require dependent types to formalise in terms of type theory.

On the other hand, things are in some ways simpler, because soundness and completeness are only required with respect to correct serialisation and deserialisation of data, not with respect to correct execution of code.

Then there is the fact that often a schema language is designed to express more than just a true/false validation process, but to add extra metadata to types for reflection by various tools / for various purposes, eg:

• Serialisation and deserialisation tools for various programming languages
• Hypertext clients (see eg the hyper-schema extensions to json-schema)
• Data persistence tools
• Even simple UI tools like admin form generators

Wonder if anyone here has any good references on this stuff, in particular any attempts to formalise semantics and prove soundness etc for such a language? (FYI I'm interested in attempting this for a YAML or JSON-based schema language)

Cheers!
-Matt