Re: What does TYPE SAFE mean?

Type safety has a formal definition and safety when applied to OCaml has a slightly different definition. Basically, Type safety has two major lemmas: that type safe programs do not enter stuck states (progress), and that if a well typed term enters a step of evaluation that it too is also well typed (preservation). This and other formal foundations allow for a much greater expanse of lemmas and other details about type safety of expressions and the property that holds once you establish that, but I leave that to the literature.
OCaml strives to be type safe, but does not have a formal proof of such that I know of. In fact, there is an escape hatch in almost every mainstream language, allowing both type coersions to take place and to execute C functions. In addition, the virtual machine and the garbage collector are undoubtedly also authored in C. Although fantastically programmed, you must *trust* that the implementation is correct and devoid of catastrophic control flow highjack vulnerabilities every time you run a piece of software derived of the OCaml compiler suite/ecosystem. However, I would posit that I don't quite see much of an escape hatch presiding within either the language vernacular or the module system, as I am pretty sure that the only instantiable non-well typed instances that will be admitted are those types that are uninhabited. There isn't computation that can take place within an uninhabited type that I know of, therefore a hack against them system would almost certainly have to take place in one of the following:

At the virtual machine/GC level
At the compiler implementation level
At an instance of faulty escape hatch usage 
At a fundamental nuance regarding intrinsics deeply rooted within some type theoretic basis that escape the attention of the typing judgements instantiated by the compiler within the vernacular (either the module language or otherwise). 

    On Saturday, February 13, 2016 2:01 AM, "Douglas Lewit [email protected] [ocaml_beginners]" <[email protected]> wrote:
 

     What do people mean when they say that Ocaml is a "type safe" language?
Thanks,
Douglas.
  #yiv9037050906 #yiv9037050906 -- #yiv9037050906ygrp-mkp {border:1px solid #d8d8d8;font-family:Arial;margin:10px 0;padding:0 10px;}#yiv9037050906 #yiv9037050906ygrp-mkp hr {border:1px solid #d8d8d8;}#yiv9037050906 #yiv9037050906ygrp-mkp #yiv9037050906hd {color:#628c2a;font-size:85%;font-weight:700;line-height:122%;margin:10px 0;}#yiv9037050906 #yiv9037050906ygrp-mkp #yiv9037050906ads {margin-bottom:10px;}#yiv9037050906 #yiv9037050906ygrp-mkp .yiv9037050906ad {padding:0 0;}#yiv9037050906 #yiv9037050906ygrp-mkp .yiv9037050906ad p {margin:0;}#yiv9037050906 #yiv9037050906ygrp-mkp .yiv9037050906ad a {color:#0000ff;text-decoration:none;}#yiv9037050906 #yiv9037050906ygrp-sponsor #yiv9037050906ygrp-lc {font-family:Arial;}#yiv9037050906 #yiv9037050906ygrp-sponsor #yiv9037050906ygrp-lc #yiv9037050906hd {margin:10px 0px;font-weight:700;font-size:78%;line-height:122%;}#yiv9037050906 #yiv9037050906ygrp-sponsor #yiv9037050906ygrp-lc .yiv9037050906ad {margin-bottom:10px;padding:0 0;}#yiv9037050906 #yiv9037050906actions {font-family:Verdana;font-size:11px;padding:10px 0;}#yiv9037050906 #yiv9037050906activity {background-color:#e0ecee;float:left;font-family:Verdana;font-size:10px;padding:10px;}#yiv9037050906 #yiv9037050906activity span {font-weight:700;}#yiv9037050906 #yiv9037050906activity span:first-child {text-transform:uppercase;}#yiv9037050906 #yiv9037050906activity span a {color:#5085b6;text-decoration:none;}#yiv9037050906 #yiv9037050906activity span span {color:#ff7900;}#yiv9037050906 #yiv9037050906activity span .yiv9037050906underline {text-decoration:underline;}#yiv9037050906 .yiv9037050906attach {clear:both;display:table;font-family:Arial;font-size:12px;padding:10px 0;width:400px;}#yiv9037050906 .yiv9037050906attach div a {text-decoration:none;}#yiv9037050906 .yiv9037050906attach img {border:none;padding-right:5px;}#yiv9037050906 .yiv9037050906attach label {display:block;margin-bottom:5px;}#yiv9037050906 .yiv9037050906attach label a {text-decoration:none;}#yiv9037050906 blockquote {margin:0 0 0 4px;}#yiv9037050906 .yiv9037050906bold {font-family:Arial;font-size:13px;font-weight:700;}#yiv9037050906 .yiv9037050906bold a {text-decoration:none;}#yiv9037050906 dd.yiv9037050906last p a {font-family:Verdana;font-weight:700;}#yiv9037050906 dd.yiv9037050906last p span {margin-right:10px;font-family:Verdana;font-weight:700;}#yiv9037050906 dd.yiv9037050906last p span.yiv9037050906yshortcuts {margin-right:0;}#yiv9037050906 div.yiv9037050906attach-table div div a {text-decoration:none;}#yiv9037050906 div.yiv9037050906attach-table {width:400px;}#yiv9037050906 div.yiv9037050906file-title a, #yiv9037050906 div.yiv9037050906file-title a:active, #yiv9037050906 div.yiv9037050906file-title a:hover, #yiv9037050906 div.yiv9037050906file-title a:visited {text-decoration:none;}#yiv9037050906 div.yiv9037050906photo-title a, #yiv9037050906 div.yiv9037050906photo-title a:active, #yiv9037050906 div.yiv9037050906photo-title a:hover, #yiv9037050906 div.yiv9037050906photo-title a:visited {text-decoration:none;}#yiv9037050906 div#yiv9037050906ygrp-mlmsg #yiv9037050906ygrp-msg p a span.yiv9037050906yshortcuts {font-family:Verdana;font-size:10px;font-weight:normal;}#yiv9037050906 .yiv9037050906green {color:#628c2a;}#yiv9037050906 .yiv9037050906MsoNormal {margin:0 0 0 0;}#yiv9037050906 o {font-size:0;}#yiv9037050906 #yiv9037050906photos div {float:left;width:72px;}#yiv9037050906 #yiv9037050906photos div div {border:1px solid #666666;height:62px;overflow:hidden;width:62px;}#yiv9037050906 #yiv9037050906photos div label {color:#666666;font-size:10px;overflow:hidden;text-align:center;white-space:nowrap;width:64px;}#yiv9037050906 #yiv9037050906reco-category {font-size:77%;}#yiv9037050906 #yiv9037050906reco-desc {font-size:77%;}#yiv9037050906 .yiv9037050906replbq {margin:4px;}#yiv9037050906 #yiv9037050906ygrp-actbar div a:first-child {margin-right:2px;padding-right:5px;}#yiv9037050906 #yiv9037050906ygrp-mlmsg {font-size:13px;font-family:Arial, helvetica, clean, sans-serif;}#yiv9037050906 #yiv9037050906ygrp-mlmsg table {font-size:inherit;font:100%;}#yiv9037050906 #yiv9037050906ygrp-mlmsg select, #yiv9037050906 input, #yiv9037050906 textarea {font:99% Arial, Helvetica, clean, sans-serif;}#yiv9037050906 #yiv9037050906ygrp-mlmsg pre, #yiv9037050906 code {font:115% monospace;}#yiv9037050906 #yiv9037050906ygrp-mlmsg * {line-height:1.22em;}#yiv9037050906 #yiv9037050906ygrp-mlmsg #yiv9037050906logo {padding-bottom:10px;}#yiv9037050906 #yiv9037050906ygrp-msg p a {font-family:Verdana;}#yiv9037050906 #yiv9037050906ygrp-msg p#yiv9037050906attach-count span {color:#1E66AE;font-weight:700;}#yiv9037050906 #yiv9037050906ygrp-reco #yiv9037050906reco-head {color:#ff7900;font-weight:700;}#yiv9037050906 #yiv9037050906ygrp-reco {margin-bottom:20px;padding:0px;}#yiv9037050906 #yiv9037050906ygrp-sponsor #yiv9037050906ov li a {font-size:130%;text-decoration:none;}#yiv9037050906 #yiv9037050906ygrp-sponsor #yiv9037050906ov li {font-size:77%;list-style-type:square;padding:6px 0;}#yiv9037050906 #yiv9037050906ygrp-sponsor #yiv9037050906ov ul {margin:0;padding:0 0 0 8px;}#yiv9037050906 #yiv9037050906ygrp-text {font-family:Georgia;}#yiv9037050906 #yiv9037050906ygrp-text p {margin:0 0 1em 0;}#yiv9037050906 #yiv9037050906ygrp-text tt {font-size:120%;}#yiv9037050906 #yiv9037050906ygrp-vital ul li:last-child {border-right:none !important;}#yiv9037050906