[langsec-discuss] Enforcing validation layer with types
will.sargent at gmail.com
Fri Jan 4 23:17:14 UTC 2013
On Jan 3, 2013, at 3:51 PM, David-Sarah Hopwood <david-sarah at jacaranda.org> wrote:
> On 03/01/13 22:43, William Sargent wrote:
>> It's not the case that the type is a label that partially constraints eligible actions. Types are a way of constructing proofs to the compiler. For example, you can specify a game of Tic Tac Toe at compile time using the type system:
> That depends on the type system and other aspects of the language, but
> the link above isn't a valid demonstration of it.
You've got a point -- Scala isn't exactly Coq or Agda.
Still, this is pretty awesome:
More information about the langsec-discuss