[langsec-discuss] Enforcing validation layer with types

William Sargent 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:
>> 
>> http://blog.tmorris.net/understanding-practical-api-design-static-typing-and-functional-programming/
> 
> 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:

http://blog.vasilrem.com/tic-tac-toe-api-with-phantom-types

Will.


More information about the langsec-discuss mailing list