{"id":395,"date":"2014-08-05T07:15:41","date_gmt":"2014-08-05T12:15:41","guid":{"rendered":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/?p=395"},"modified":"2014-08-05T08:55:54","modified_gmt":"2014-08-05T13:55:54","slug":"type-safety","status":"publish","type":"post","link":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/","title":{"rendered":"What is type safety?"},"content":{"rendered":"

In response to my previous post defining memory safety<\/a>\u00a0(for C), one commenter suggested it would be nice to have a post explaining type safety. Type safety is pretty well understood, but it’s still not something you can easily pin down. In particular, when someone says, “Java is a type-safe language,” what do they mean, exactly? Are all type-safe languages “the same” in some way? What is type safety getting you, for particular languages, and in general?<\/p>\n

In fact, what type safety means depends on\u00a0language type system’s definition. In the simplest\u00a0case, type safety ensures that\u00a0program behaviors are well defined. More generally,\u00a0as I discuss in this post, a language’s\u00a0type system\u00a0can be a powerful tool for reasoning about the correctness and security of its programs, and as such the development of novel type systems is a rich area of research.<\/p>\n

<\/p>\n

Basic Type Safety<\/h2>\n

An intuitive\u00a0notion of type safety is pithily summarized by the phrase, “Well typed\u00a0<\/strong>programs\u00a0cannot go wrong<\/strong><\/i>.” This phrase was coined by\u00a0Robin Milner<\/a>\u00a0in his 1978 paper,\u00a0A Theory of Type Polymorphism in Programming<\/a>.\u00a0Let’s deconstruct this phrase and\u00a0define its parts, considering the second part first.<\/p>\n

Going wrong<\/h3>\n

Programming languages are defined by their syntax<\/em> — what programs you’re allowed to write down\u00a0—\u00a0and semantics<\/em> — what those programs\u00a0mean. A problem all languages face is that there are many programs that are syntactically valid but are semantically problematic. A classic English example is Chomsky’s “Colorless green ideals sleep furiously”—perfectly syntactically correct, but meaningless. A\u00a0example in the OCaml programming language\u00a0is 1 + “foo”<\/strong>; according to the language’s semantics, such a program has no meaning. Another example is { char buf[4]; buf[4] = ‘x’ }<\/strong> in C: the write to index 4 is outside the declared bounds of the buffer, and the language specification deems this action to be\u00a0undefined, i.e., meaningless. If we were to run such meaningless programs, we could say that they would\u00a0go wrong.<\/em><\/p>\n

Well typed \u27f9 Cannot go wrong<\/h3>\n

In a type-safe language, the language’s type system<\/em> is a particular way of ensuring that\u00a0only the\u00a0“right” (non-wrong) programs go through. In particular, we say a program (or program phase) is well typed<\/em> if the type system deems it acceptable, and type safety ensures that well typed programs never go wrong: they will have a (well defined) meaning. The following picture\u00a0visualizes what’s going on.<\/p>\n

\"typing-venn\"<\/a><\/p>\n

In a type safe language, well typed programs are a subset of the well defined programs, which are themselves a subset of all possible (syntactically valid) programs.<\/p>\n

Which languages are type safe?<\/h2>\n

Let’s now\u00a0consider whether some popular languages<\/a>\u00a0are type safe.\u00a0We will see that for different languages, type safety might mean different things.<\/p>\n

C and C++: not<\/em> type safe<\/strong>. C’s standard\u00a0type system does not rule out programs that the standard (and common practice) considers meaningless, e.g., programs that write off the end of a buffer.[ref] C is also not memory safe<\/a>; in effect, the undefined behaviors that memory safety rules out are\u00a0a subset of the undefined behaviors ruled out by type safety.[\/ref] So, for C, well typed programs can go wrong. C++ is (morally) a superset of C, and so it inherits C’s lack of type safety.<\/p>\n

Java, C#:\u00a0type safe<\/strong> (probably). While it is quite difficult to ascertain whether a full-blown language implementation is type safe (e.g., an early version of Java generics was buggy<\/a>), formalizations of smaller, hopefully-representative languages (like Featherweight Java<\/a>) are type safe.[ref] While full-scale languages rarely receive the same attention as smaller core calculi<\/em> that represent them, in 1997,\u00a0Standard ML (SML) was formally specified<\/a> — both its semantics and type system — and proven to be type safe. Later work mechanized the metatheory of SML<\/a>, adding further assurance to this result. This was landmark work to prove that a full-scale language was indeed type safe.[\/ref] Interestingly, type safety hinges on the fact that behaviors that C’s semantics deem as undefined, these languages give meaning to. Most notably, a program in C that accesses an array out of bounds has no meaning, but in Java and C# it does: this program will throw an ArrayBoundsException<\/em>.<\/p>\n

Python, Ruby<\/strong>: type safe<\/strong> (arguably).\u00a0Python or Ruby are often referred to\u00a0as dynamically typed languages<\/em>, which throw exceptions to signal type errors occurring during execution: Just like\u00a0Java throws an ArrayBoundsException<\/em> on an array overflow at run-time, Ruby will throw an exception if you try to add an integer and a string. In both cases, this behavior is prescribed by the language semantics, and therefore the programs are well defined. In fact, the language semantics gives meaning to all programs, so the well defined<\/em> and all<\/em> circles of our diagram coincide. As such, we can think of these languages as type safe according to the null<\/em> type system,[ref]Sometimes \u00a0languages like Python and Ruby are characterized as\u00a0uni-typed<\/em>, meaning that for the purposes of type checking, all objects in the language have one type that accepts all operations, but these\u00a0operations\u00a0may fail at run-time. Programmers may not think of the languages this way, though<\/a>.[\/ref] which accepts\u00a0all programs, none of which go\u00a0wrong (making all three circles coincide). Hence: type safety.<\/p>\n

This conclusion\u00a0might seem strange.\u00a0In Java, if program o.m()<\/strong> is deemed well typed, then type safety ensures that o<\/strong> is an object that has a no-argument method m<\/strong>, and so the call will always succeed. In Ruby, the same program o.m()<\/strong> is always<\/em> deemed well typed by Ruby’s\u00a0(null) type system, but when we run it, we have no guarantee that o<\/strong>\u00a0defines the method m<\/strong>, and as such either the call will succeed, or it will\u00a0result in an exception.<\/p>\n

In short, type safety does not mean one thing. What it ensures depends on the language semantics, which implicitly defines wrong behavior. In Java, calling a nonexistent\u00a0method is wrong. In Ruby, it is not: doing so will simply produce an exception.[ref]You could imagine building an alternative type system to rule out some of Ruby’s\u00a0run-time errors; indeed that’s what the Diamondback Ruby<\/a> project tries to do.[\/ref]<\/p>\n

Beyond the Basics<\/h2>\n

Generic type safety is useful: without it, we have no guarantee that the programs we run are properly defined,\u00a0in which case they could do essentially\u00a0anything. C\/C++’s\u00a0allowance of undefined behavior is the source of a myriad security exploits, from\u00a0stack smashing<\/a> to\u00a0format string attacks<\/a>. Such\u00a0exploits\u00a0are not possible in\u00a0type safe languages.<\/p>\n

On the other hand, as our discussion above about Ruby and Java illustrates, not all type systems are created equal: some can ensure properties that\u00a0others cannot. As such, we should\u00a0not just ask whether a language is type safe; we should ask what type safety actually buys you. We’ll finish out this post with a few examples of what type systems can do, drawing from a rich landscape of ongoing research.<\/p>\n

Narrowing the gap<\/h3>\n

The well typed<\/em> and well defined<\/em> circles in our diagram do not match up; in the gap between them are programs that are well defined but the type system nevertheless rejects. As an example, most type systems will reject the\u00a0following program:<\/p>\n

\r\nif (p) x = 5;\r\n  else x = "hello";\r\nif (p) return x+5;\r\n  else return strlen(x);\r\n<\/pre>\n
This program will always\u00a0return an integer, but the type system may reject it because the variable x<\/strong> is used as both an int<\/strong> and a string<\/strong>. Drawing an analogy\u00a0with\u00a0static analysis, as discussed previously in the context of the Heartbleed bug<\/a>, type systems are sound<\/em> but incomplete<\/em>. This incompleteness is a source of frustration for\u00a0programmers, (and may be one reason driving them to use dynamic languages like Python and Ruby<\/a>).\u00a0One remedy is to design type systems that narrow the gap, accepting more programs.<\/p>\n
As an\u00a0example if this process in action, Java’s type system was extended in version 1.5 with the notion of\u00a0generics<\/em><\/a>. Whereas in Java\u00a01.4 you might need\u00a0to use\u00a0a cast to convince the type system to accept a program, in Java 1.5 this cast might\u00a0not be needed. As another example, consider the lambda calculus<\/a>, the basis of functional programming languages. The simple type system<\/a> for the\u00a0lambda calculus accepts strictly fewer programs than Milner’s polymorphic type system<\/a>, which accepts fewer programs than a type system that\u00a0supports Rank-2 (or higher) polymorphism<\/a>. Designing type systems that are expressive (more complete) and<\/em> usable is a rich area of research.<\/p>\n
Enforcing invariants<\/h3>\n
Typical languages have types like int<\/strong> and string<\/strong>. Type safety will ensure that a program expression that claims to\u00a0be an int<\/strong> actually is: it will evaluate to -1, 2, 47, etc. at run-time.\u00a0But we don’t need to stop with int<\/strong>: A type system can support far richer types and thereby express more interesting properties about program expressions.<\/p>\n
For example, there has been much recent interest in the research community in\u00a0refinement types<\/em>, which\u00a0refine\u00a0the set of a type’s possible values using\u00a0logical\u00a0formulae. The type\u00a0{v: int | 0\u00a0<= v}<\/strong>\u00a0refines the type int<\/strong> with formula 0 <= v<\/strong>, and in effect defines the type of\u00a0non-negative integers. Refinement types allow programmers to express data structure invariants\u00a0in the\u00a0types of those data structures, and due to type safety be assured that those invariants will always hold. Refinement type systems have been developed for Haskell and F# (called\u00a0Liquid Haskell<\/a> and F7,<\/a>\u00a0respectively), among other languages.<\/p>\n
As another example, we can use a\u00a0type system\u00a0to ensure data race<\/a> freedom by enforcing\u00a0the invariant that a shared variable is only ever accessed by a thread that holds the lock that guards that variable. The type of a shared variable describes the locks that protect it. Types for safe locking<\/a>\u00a0was first proposed by Abadi and Flanagan, and implementations have been developed for Java<\/a>\u00a0and C (Locksmith<\/a>).<\/p>\n
There are many other examples, with type systems designed to restrict the use of tainted data<\/a>, to prevent the release of private information<\/a>, to ensure object usage follows a strict protocol called type state<\/em><\/a> (e.g., so that an object is not used after it is freed), and more.<\/p>\n
Type abstraction and information hiding<\/h3>\n
Many programming languages aim to allow programmers to enforce data abstraction <\/em>(sometimes called\u00a0information hiding<\/em>).\u00a0These languages permit writing\u00a0abstractions, like classes or modules or functions, that keep their internals hidden from the client code that uses them. Doing so leads to more robust and maintainable programs, because the internals can be changed without affecting the client code.<\/p>\n
Type systems can play a crucial role in enforcing abstraction. For example, with the aid of a well designed type system, we can prove representation independence<\/a>, which says that programs only depend on the behavior of an abstraction, not on the way it is implemented. Type-enforced\u00a0abstraction can also be an enabler of\u00a0free theorems<\/a>, as Wadler elegantly showed. The late\u00a0John Reynolds<\/a>\u00a0did groundbreaking work on types and abstraction, most notably described in his 1983 paper, Types, Abstraction, and Parametric Polymorphism<\/a>. In this paper he famously\u00a0states\u00a0“type structure is a syntactic discipline for maintaining\u00a0levels of\u00a0abstraction,<\/em>” positing\u00a0that types have\u00a0a fundamental<\/em> role in building maintainable systems.<\/p>\n
Parting thought<\/h2>\n
Type safety is an important property. At the least, a type safe language guarantees its programs are well defined. This guarantee is\u00a0necessary for reasoning about what programs might do, which is particularly important when security is a concern. But type systems can do more, forming a foundation for reasoning about programs, ensuring that they enforce invariants, and maintain abstractions. As software is becoming ever more pervasive and more complicated, type systems are\u00a0an important tool for ensuring the systems we rely on are trustworthy and secure.<\/p>\n
If you are interested in learning more about type systems, I’d recommend starting with Benjamin Pierce<\/a>‘s books, Types and Programming Languages<\/a>, and Advanced Topics in Types and Programming Languages<\/a>.<\/p>\n
Thanks to Matthew Hammer<\/a>, Jeff Foster<\/a>, and David Van Horn<\/a> for comments and suggestions on drafts of this post.<\/p>\n","protected":false},"excerpt":{"rendered":"
In response to my previous post defining memory safety\u00a0(for C), one commenter suggested it would be nice to have a post explaining type safety. Type safety is pretty well understood, but it’s still not something you can easily pin down. … Continue reading →<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_monsterinsights_skip_tracking":false,"_monsterinsights_sitenote_active":false,"_monsterinsights_sitenote_note":"","_monsterinsights_sitenote_category":0,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":true,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2},"jetpack_post_was_ever_published":false},"categories":[32,19,26,3,31],"tags":[],"class_list":["post-395","post","type-post","status-publish","format-standard","hentry","category-dynamic-languages","category-pl-in-practice","category-semantics","category-softsec","category-types"],"yoast_head":"\nWhat is type safety? - The PL Enthusiast<\/title>\n<meta name=\"description\" content=\"Type safety is the property of a programming language, ensuring its programs are well defined and creating a foundation for reasoning.\" \/>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"What is type safety? - The PL Enthusiast\" \/>\n<meta property=\"og:description\" content=\"Type safety is the property of a programming language, ensuring its programs are well defined and creating a foundation for reasoning.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/\" \/>\n<meta property=\"og:site_name\" content=\"The Programming Languages Enthusiast\" \/>\n<meta property=\"article:published_time\" content=\"2014-08-05T12:15:41+00:00\" \/>\n<meta property=\"article:modified_time\" content=\"2014-08-05T13:55:54+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-content\/uploads\/2014\/08\/typing-venn.jpg\" \/>\n<meta name=\"author\" content=\"Michael Hicks\" \/>\n<meta name=\"twitter:label1\" content=\"Written by\" \/>\n\t<meta name=\"twitter:data1\" content=\"Michael Hicks\" \/>\n\t<meta name=\"twitter:label2\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data2\" content=\"10 minutes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\\\/\\\/schema.org\",\"@graph\":[{\"@type\":\"Article\",\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/2014\\\/08\\\/05\\\/type-safety\\\/#article\",\"isPartOf\":{\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/2014\\\/08\\\/05\\\/type-safety\\\/\"},\"author\":{\"name\":\"Michael Hicks\",\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/#\\\/schema\\\/person\\\/7d875a015cb2e83e9cd476df91028d5d\"},\"headline\":\"What is type safety?\",\"datePublished\":\"2014-08-05T12:15:41+00:00\",\"dateModified\":\"2014-08-05T13:55:54+00:00\",\"mainEntityOfPage\":{\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/2014\\\/08\\\/05\\\/type-safety\\\/\"},\"wordCount\":2026,\"commentCount\":40,\"image\":{\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/2014\\\/08\\\/05\\\/type-safety\\\/#primaryimage\"},\"thumbnailUrl\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/wp-content\\\/uploads\\\/2014\\\/08\\\/typing-venn.jpg\",\"articleSection\":[\"Dynamic languages\",\"PL in practice\",\"Semantics\",\"Software Security\",\"Types\"],\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"CommentAction\",\"name\":\"Comment\",\"target\":[\"http:\\\/\\\/www.pl-enthusiast.net\\\/2014\\\/08\\\/05\\\/type-safety\\\/#respond\"]}]},{\"@type\":\"WebPage\",\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/2014\\\/08\\\/05\\\/type-safety\\\/\",\"url\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/2014\\\/08\\\/05\\\/type-safety\\\/\",\"name\":\"What is type safety? - The PL Enthusiast\",\"isPartOf\":{\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/#website\"},\"primaryImageOfPage\":{\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/2014\\\/08\\\/05\\\/type-safety\\\/#primaryimage\"},\"image\":{\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/2014\\\/08\\\/05\\\/type-safety\\\/#primaryimage\"},\"thumbnailUrl\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/wp-content\\\/uploads\\\/2014\\\/08\\\/typing-venn.jpg\",\"datePublished\":\"2014-08-05T12:15:41+00:00\",\"dateModified\":\"2014-08-05T13:55:54+00:00\",\"author\":{\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/#\\\/schema\\\/person\\\/7d875a015cb2e83e9cd476df91028d5d\"},\"description\":\"Type safety is the property of a programming language, ensuring its programs are well defined and creating a foundation for reasoning.\",\"breadcrumb\":{\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/2014\\\/08\\\/05\\\/type-safety\\\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"http:\\\/\\\/www.pl-enthusiast.net\\\/2014\\\/08\\\/05\\\/type-safety\\\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/2014\\\/08\\\/05\\\/type-safety\\\/#primaryimage\",\"url\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/wp-content\\\/uploads\\\/2014\\\/08\\\/typing-venn.jpg\",\"contentUrl\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/wp-content\\\/uploads\\\/2014\\\/08\\\/typing-venn.jpg\",\"width\":224,\"height\":224},{\"@type\":\"BreadcrumbList\",\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/2014\\\/08\\\/05\\\/type-safety\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"What is type safety?\"}]},{\"@type\":\"WebSite\",\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/#website\",\"url\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/\",\"name\":\"The Programming Languages Enthusiast\",\"description\":\"Developments in PL, and why they matter\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"en-US\"},{\"@type\":\"Person\",\"@id\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/#\\\/schema\\\/person\\\/7d875a015cb2e83e9cd476df91028d5d\",\"name\":\"Michael Hicks\",\"image\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/dd0371ad9a0cb821df683b5d6a6cccc911e6e2af1778f28b77e8c90b0c319d14?s=96&d=mm&r=g\",\"url\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/dd0371ad9a0cb821df683b5d6a6cccc911e6e2af1778f28b77e8c90b0c319d14?s=96&d=mm&r=g\",\"contentUrl\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/dd0371ad9a0cb821df683b5d6a6cccc911e6e2af1778f28b77e8c90b0c319d14?s=96&d=mm&r=g\",\"caption\":\"Michael Hicks\"},\"sameAs\":[\"http:\\\/\\\/www.cs.umd.edu\\\/~mwh\\\/\"],\"url\":\"http:\\\/\\\/www.pl-enthusiast.net\\\/author\\\/mwh\\\/\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"What is type safety? - The PL Enthusiast","description":"Type safety is the property of a programming language, ensuring its programs are well defined and creating a foundation for reasoning.","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/","og_locale":"en_US","og_type":"article","og_title":"What is type safety? - The PL Enthusiast","og_description":"Type safety is the property of a programming language, ensuring its programs are well defined and creating a foundation for reasoning.","og_url":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/","og_site_name":"The Programming Languages Enthusiast","article_published_time":"2014-08-05T12:15:41+00:00","article_modified_time":"2014-08-05T13:55:54+00:00","og_image":[{"url":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-content\/uploads\/2014\/08\/typing-venn.jpg","type":"","width":"","height":""}],"author":"Michael Hicks","twitter_misc":{"Written by":"Michael Hicks","Est. reading time":"10 minutes"},"schema":{"@context":"https:\/\/fd.xuwubk.eu.org:443\/https\/schema.org","@graph":[{"@type":"Article","@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/#article","isPartOf":{"@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/"},"author":{"name":"Michael Hicks","@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/#\/schema\/person\/7d875a015cb2e83e9cd476df91028d5d"},"headline":"What is type safety?","datePublished":"2014-08-05T12:15:41+00:00","dateModified":"2014-08-05T13:55:54+00:00","mainEntityOfPage":{"@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/"},"wordCount":2026,"commentCount":40,"image":{"@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/#primaryimage"},"thumbnailUrl":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-content\/uploads\/2014\/08\/typing-venn.jpg","articleSection":["Dynamic languages","PL in practice","Semantics","Software Security","Types"],"inLanguage":"en-US","potentialAction":[{"@type":"CommentAction","name":"Comment","target":["https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/#respond"]}]},{"@type":"WebPage","@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/","url":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/","name":"What is type safety? - The PL Enthusiast","isPartOf":{"@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/#website"},"primaryImageOfPage":{"@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/#primaryimage"},"image":{"@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/#primaryimage"},"thumbnailUrl":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-content\/uploads\/2014\/08\/typing-venn.jpg","datePublished":"2014-08-05T12:15:41+00:00","dateModified":"2014-08-05T13:55:54+00:00","author":{"@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/#\/schema\/person\/7d875a015cb2e83e9cd476df91028d5d"},"description":"Type safety is the property of a programming language, ensuring its programs are well defined and creating a foundation for reasoning.","breadcrumb":{"@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/"]}]},{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/#primaryimage","url":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-content\/uploads\/2014\/08\/typing-venn.jpg","contentUrl":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-content\/uploads\/2014\/08\/typing-venn.jpg","width":224,"height":224},{"@type":"BreadcrumbList","@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/2014\/08\/05\/type-safety\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/"},{"@type":"ListItem","position":2,"name":"What is type safety?"}]},{"@type":"WebSite","@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/#website","url":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/","name":"The Programming Languages Enthusiast","description":"Developments in PL, and why they matter","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"en-US"},{"@type":"Person","@id":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/#\/schema\/person\/7d875a015cb2e83e9cd476df91028d5d","name":"Michael Hicks","image":{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/fd.xuwubk.eu.org:443\/https\/secure.gravatar.com\/avatar\/dd0371ad9a0cb821df683b5d6a6cccc911e6e2af1778f28b77e8c90b0c319d14?s=96&d=mm&r=g","url":"https:\/\/fd.xuwubk.eu.org:443\/https\/secure.gravatar.com\/avatar\/dd0371ad9a0cb821df683b5d6a6cccc911e6e2af1778f28b77e8c90b0c319d14?s=96&d=mm&r=g","contentUrl":"https:\/\/fd.xuwubk.eu.org:443\/https\/secure.gravatar.com\/avatar\/dd0371ad9a0cb821df683b5d6a6cccc911e6e2af1778f28b77e8c90b0c319d14?s=96&d=mm&r=g","caption":"Michael Hicks"},"sameAs":["https:\/\/fd.xuwubk.eu.org:443\/http\/www.cs.umd.edu\/~mwh\/"],"url":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/author\/mwh\/"}]}},"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-json\/wp\/v2\/posts\/395","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-json\/wp\/v2\/comments?post=395"}],"version-history":[{"count":10,"href":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-json\/wp\/v2\/posts\/395\/revisions"}],"predecessor-version":[{"id":430,"href":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-json\/wp\/v2\/posts\/395\/revisions\/430"}],"wp:attachment":[{"href":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-json\/wp\/v2\/media?parent=395"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-json\/wp\/v2\/categories?post=395"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/fd.xuwubk.eu.org:443\/http\/www.pl-enthusiast.net\/wp-json\/wp\/v2\/tags?post=395"}],"curies":[{"name":"wp","href":"https:\/\/fd.xuwubk.eu.org:443\/https\/api.w.org\/{rel}","templated":true}]}}