21 ms·

Types Are The Truth

132 points by mrbbk 12y ago

webmaven 12y ago
Hello, doppleganger! (I'm http://michaelbernstein.com http://michaelbernstein.com)
- mrbbk 12y ago
  Haha, hi there. As you can imagine, I've been to your homepage before.
  - webmaven 12y ago
    It's actually out of date, I'm currently in Kansas City. Have you also been confused with http://hci.stanford.edu/msb/ http://hci.stanford.edu/msb/ or http://michaelbernstein.biz/ http://michaelbernstein.biz/ and even http://www.mabfan.com/ http://www.mabfan.com/ at SF conventions? ;-)
- ludicast 12y ago
  kinda sad that one of you two has to die now. webmaven was here longer so my money is on his time being up.
  - webmaven 12y ago
    There can be only one! (I'd actually put my money on old age and treachery vs. youth and skill if I were you)
ufo 12y ago
> Types are there whether you want them to be or not But this only applies to typed programs, right? For every type system you come up with there will be some valid and normalizing term that cannot be typed under that type system. There is also a minor thing that came to my mind. Types are most often associated with intuitionist logics, which are about constructive provability, as opposed to classical logics, which are about "truthyness" so the title of the post is a bit misleading :)
- dllthomas 12y ago
  "But this only applies to typed programs, right? For every type system you come up with there will be some valid and normalizing term that cannot be typed under that type system." In theory, yes - I came here to make that same objection. In practice, there arises the question of whether such terms are actually ever encountered for a given type system when solving realistic problems.
  - comex 12y ago
    For most type systems, they certainly are: most reasonably large C programs contain assembly corresponding to unsafe pointers, unions, etc. that a compiler for a typical high-level language cannot emit under any circumstances (without being ridiculously intelligent). Languages like ATS and C-plus-formal-verification mostly avoid this problem at the expense of being really hard to write.
    - dllthomas 12y ago
      "most reasonably large C programs contain assembly corresponding to unsafe pointers, unions, etc." I'm not sure what you're saying here with the "corresponding to" - obviously you can write "unsafe pointers", unions, etc, right in C, and I've not really ever encountered inline assembly for the purposes of subverting the type system. I'll respond to more of your content when I'm confident I've understood you (which I don't mean as a brush off...).
      - comex 12y ago
        My response was poorly worded, but what I meant is that compilers for other languages with higher level type systems (which make more guarantees) cannot emit the same assembly as a C compiler, not that assembly is needed to subvert C's type system.
        steveklabnik 12y ago
        Why not? Can you show me an example of what you mean? EDIT: I think the difference here is between 'types' and 'tags'. Types are at compile time. Tags are at runtime.
dkarapetyan 12y ago
Yes, type erasure is neat and a bit of thinking will make it obvious why proving static properties does not require run time checks if the transformations you perform on your program preserve those static properties. I disagree with the author's claim though that types are everywhere. Types in fact are extra structure that is hoisted onto programs. At the end of the day the machine knows nothing about the types and will shuttle bytes back and forth all day long. Furthermore, types restrict the universe of computation and there are examples of programs that are not well-typed but don't go wrong when evaluated.
- mtdewcmu 12y ago
  I wonder if type erasure is profound, or if it only sounds profound after being hypnotized by type theory.
  - dkarapetyan 12y ago
    Don't get me wrong I think type theory is really cool. In fact any kind of theory that makes me a better programmer is cool. That's one of the reasons TypeScript right now is one of my favorite languages. It is the perfect balance between the prototyping power of dynamic languages and the awesome static guarantees of statically typed languages. The best part is that the type system does not get in the way when I'm prototyping and actually starts to help out when I have the design fleshed out. I just wish more languages supported that kind of type system because sometimes I really miss the static checks when writing stuff in Ruby and Python.
    - mtdewcmu 12y ago
      What I think is cool is getting computers to do things that are interesting. Types don't do anything. I find them hard to get excited about.
      - the_af 12y ago
        What do you mean "types don't do anything"? Are you seriously going to argue that? I don't know many people in the programming or CS fields who believe that. What some people believe is that there are type systems too onerous for the benefits they bring (which is, of course, debatable). Following your line of thought, one could say that the textual representation of your program "doesn't do anything" either, and neither does the syntax or the IDE/editor you use. So none of it matters. But of course it wouldn't be true -- all those things are useful tools that help you write software that does cool things. edit: thought of an even better example: tests. Tests "don't do anything". They are not directly related to the cool stuff we want to do with our computers. But who is going to argue that we shouldn't write any tests?
eudox 12y ago
The site is eerily similar to http://www.jonmsterling.com/index.html http://www.jonmsterling.com/index.html You two could hit it off or something.
dicroce 12y ago
If you were building a sandcastle, a type system is like plastic forms in the shape of castle components (walls, towers, etc)... They help you create a better sandcastle... This article was essentially saying: "You can remove the forms when you are done and your sandcastle will still stand."
- taeric 12y ago
  By that same analogy, building up a sand castle by only using those molds is a ridiculously hard way to build some castles.
  - Lambdanaut 12y ago
    Fortunately some languages allow you to construct your own custom molds within the language itself.
    - taeric 12y ago
      Right, I was not trying to make an absolute "type systems are bad" statement. Just pointing out that the analogy can be used to cut both ways. :) Indeed, I think the analogy has pretty good legs. Consider, if you are working with cast iron, molds are the way to go.
    - aikah 12y ago
      and in others,one isnt even allowed to use his hands...
      - kazagistar 12y ago
        Your hands are your mind... you think the types, check the types, and erase them, but do all of it briefly, while playing with that part, and then move away. Compiled languages are like building a bunch of plaster mold, and then just doing the castle in one step. Optional typing, or using Any types and casting, is like using molds for a nice foundation, and using your hands to add little bits on top.
TheLoneWolfling 12y ago
Personally, I wish that type systems allowed for arbitrary pure (as in "same input -> same output") code to define what is and isn't a valid instance of a type at compile time. Being able to declare a function that is only valid for, say, power of two inputs (say: a hashmap's initial size, when the hashmap is using a bitwise and for wrapping) and having it actually enforced at compile time would be very useful. I mean, even range types are useful.
- Ixiaus 12y ago
  Dependent Types? Check out Idris.
  - TheLoneWolfling 12y ago
    I shall have to. That being said, I don't care much for Haskell-based syntax.
    - saryant 12y ago
      Dotty is another option, a potential successor to Scala: https://github.com/lampepfl/dotty https://github.com/lampepfl/dotty
    - ixmatus 12y ago
      To each his own. I rarely hear fluent Haskellers say they don't care for the syntax though; if you haven't really gotten far enough to write production code in Haskell that leverages Haskell's powerful abstraction features, then you should and you might find the syntax growing on you. The syntax is nice because it enables the programmer to express software in a terse way, generally favoring the types as documentation and a strong mental model to understand the abstraction.
    - kazagistar 12y ago
      It is also a lot of work to prove your code. Here, have a nice Idris video to give you a taste: https://www.youtube.com/watch?v=P82dqVrS8ik https://www.youtube.com/watch?v=P82dqVrS8ik
TheLoneWolfling 12y ago
Isn't type erasure just a rather limited subclass of compiler optimization, and as such comes "for free" without having to explicitly code for it? The compiler frontend can leave in all type checks, having most of them can be removed by the optimizer, the same way you can remove any sort of redundant check (a default case in a switch statement over an enumeration, etc, etc) That being said, general type erasure can have (massive) problems. Look at Java.
- lmm 12y ago
  I'd say Java's type erasure has on the whole been massively successful (and it's allowed integration with e.g. Scala that a more reified type system might make difficult). What do you see as wrong with it?
  - TheLoneWolfling 12y ago
    Too much wrestling with generics. For example, having to use a varargs hack just to make a T[] (that's an array of a a generic type). Or not being able to call T.class Or not being able to use instanceof T. Or having a Object[] that crashes at runtime when you try to put an Object in it. Or not being able to overload a method based on if it's passed a List<Foo> or List<Bar>. (Also applies to interfaces like Comparable, etc. There's no good way of going "this is a Comparable<Foo> and a Comparable<Bar>, but not a Comparable<Baz>.) Or for that matter, trying to pass an int[] to something that expects an Integer[], or vice versa. Or for that matter, someone passing in a List into your parameter expecting List<Foo> and crashing at runtime because it actually was a List<Bar>.
    - dgreensp 12y ago
      Java uses type erasure purely as a strategy for implementing generics. Combining type erasure and dispatch-on-type definitely produces some odd edges.
    - mcosta 12y ago
      It is ugly but you can make many of that things making all constructors request a paramter Class<T> cls. One thing you learn using java is not moving arrays around. The comparator stuff is true. Make the compiler to fail if you pass raw classes. A List is not a List<Foo> and in some cases is not a List<?> (where List is a class of <T extends Foo>). What I miss is some kind of self type, or "return this", I do not know how to tell it. Imagine a imaginary class A: this aMethod() { stuff(); return this; ) This aMethod returns an A when invoked on an A instance or a B, B extends A, if is a B instance. Handy for builders and fluid apis: B thisIsB = new B(); thisIsB.aMethod().bMethod();
juliangamble 12y ago
Some food for thought from Rich Hickey: "Statically typed programs and programmers can certainly be as correct about the outside world as any other program/programmers can, but the type system is irrelevant in that regard. The connection between the outside world and the premises will always be outside the scope of any type system." http://www.reddit.com/r/programming/comments/lirke/simple_made_easy_by_rich_hickey_video/c2u1fgc http://www.reddit.com/r/programming/comments/lirke/simple_ma...
- Dewie 12y ago
  I was more convinced by someone who replied to that post (psnively). He seems to be saying that type systems can't model the world as we know it perfectly, in which case it sounds like a Nirvana fallacy - we can model a lot of things that we care about as programmers, so even though we can't model all of it, it still has merit. If what he is referring to is that type systems are somehow "separate" from the outside world, then it seems somewhat like saying that mathematics is a wholly abstract field. Still, though, applied mathematics has been incredibly successful. After psnively's reply, Rich decides to throw a tantrum (read: "bow out").
- gargantuan 12y ago
  Also what about protocols? Can type systems handle that. Things like: * open file * close file * read form file That can be type checked up and down it will still be broken. Is that Rich Hickey meant? Here we are dealing with a real world -- a file. And it has a protocol to access it. So in a sense we want a protocol checker not a type checker in that case...?
  - mcosta 12y ago
    I am pretty sure with a elaborate enough system with alias-forbidden types and resource managers you can do it. with file.open as f do .... alias = f // fail done // autoclose But then, is it really necessary?
  - evincarofautumn 12y ago
    Separation logic can handle that—it’s a program logic that subsumes typechecking and typestate, among other things. Your example, in pseudocode: // open : string -> file_mode -> (f : file) | f @ read * f @ close f = open "input.dat" Read // close : (f : file) | f @ read * f @ close -> () close f // getline : (f : file) | f @ read -> string | f @ read s = getline f “open” grants the “read” and “close” permissions to “f”; “close” revokes the “read” permission that “getline” requires, causing “getline” not to typecheck.
pfh 12y ago
Types Are The Truth. Values Are The Proof.
CmonDev 12y ago
"Whether your programming language "embraces" types or has a modern type system or not, these concepts are central to how programs execute, because they are a fundamental part of how computation works." - what are "modern" type systems? Was something new invented in the last 15-20 years that I had missed?
todd8 12y ago
The discussion of types here is all over the place. This is because they are handled so differently in various programming languages. Pascal included array bounds in the type annotation for arrays and subscripting was enforced (at runtime) to be withing bounds. In C (and C++) arrays are almost equivalent to pointers (the full answer is complicated see [1]) and there is a real danger of buffer overflows. Python doesn't include type annotations, but the run-time enforces strong typing, lists carry their type information and will throw an exception if subjected to a non-list operation. The type system in Haskell is perhaps the best example of a really expressive and really effective system for ensuring that the compiler can catch as many error as possible at compile time. Haskell programmers sometimes say that if a program compiles it almost always works. This is interesting, but unfortunately, types and type annotations in use today don't fully capture the formal specification needed to guarantee program correctness. Just writing down specification in preparation for a proof of correctness can be difficult. The specifications have to be expressed in a formal system, for example some form of mathematical logic like predicate calculus. Working with anything less than a formal specification is like trying to solve a mathematical set of equations without using math symbols. Natural language is just inadequate to the task. See [2]. Getting the specifications right isn't easy. I remember my first attempt at proving the correctness of a sorting program. I understood that I needed to insure that A[i] <= A[i+1] for all elements in the array, but I forgot that the final result had to include all and only the original elements (i.e. that it had to be a strict permutation of the input elements). I don't believe that type systems are currently useful for these kind of specifications and verifications of program correctness. Real programs interact with the outside world (e.g. GUI's are hard to describe mathematically). Real programs often have distributed or concurrent execution for which new logics (like Temporal Logic) may have to be employed. Proving that a program will terminate or make progress or not deadlock or not livelock or will meet some real-time constraints are all exceptionally hard. Many years ago (in the 1980's) I worked on this research area at University. I had the hope that eventually, programming would be more like an interactive exploration with a sophisticated program prover. I thought that the programmer and software-prover would work together to produce a correct program. Today, we are still programming in pretty much the same old ways as back then. The languages are much better, but it's a harder problem than I thought it was going to be. [1] http://stackoverflow.com/questions/3959705/arrays-are-pointers http://stackoverflow.com/questions/3959705/arrays-are-pointe... [2] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD667.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/E...

Types Are The Truth

132 points by mrbbk 12y ago

webmaven 12y ago

Hello, doppleganger! (I'm http://michaelbernstein.com http://michaelbernstein.com)

mrbbk 12y ago
Haha, hi there. As you can imagine, I've been to your homepage before.
- webmaven 12y ago
  It's actually out of date, I'm currently in Kansas City. Have you also been confused with http://hci.stanford.edu/msb/ http://hci.stanford.edu/msb/ or http://michaelbernstein.biz/ http://michaelbernstein.biz/ and even http://www.mabfan.com/ http://www.mabfan.com/ at SF conventions? ;-)
ludicast 12y ago
kinda sad that one of you two has to die now. webmaven was here longer so my money is on his time being up.
- webmaven 12y ago
  There can be only one! (I'd actually put my money on old age and treachery vs. youth and skill if I were you)

ufo 12y ago

> Types are there whether you want them to be or not But this only applies to typed programs, right? For every type system you come up with there will be some valid and normalizing term that cannot be typed under that type system. There is also a minor thing that came to my mind. Types are most often associated with intuitionist logics, which are about constructive provability, as opposed to classical logics, which are about "truthyness" so the title of the post is a bit misleading :)

dllthomas 12y ago
"But this only applies to typed programs, right? For every type system you come up with there will be some valid and normalizing term that cannot be typed under that type system." In theory, yes - I came here to make that same objection. In practice, there arises the question of whether such terms are actually ever encountered for a given type system when solving realistic problems.
- comex 12y ago
  For most type systems, they certainly are: most reasonably large C programs contain assembly corresponding to unsafe pointers, unions, etc. that a compiler for a typical high-level language cannot emit under any circumstances (without being ridiculously intelligent). Languages like ATS and C-plus-formal-verification mostly avoid this problem at the expense of being really hard to write.
  - dllthomas 12y ago
    "most reasonably large C programs contain assembly corresponding to unsafe pointers, unions, etc." I'm not sure what you're saying here with the "corresponding to" - obviously you can write "unsafe pointers", unions, etc, right in C, and I've not really ever encountered inline assembly for the purposes of subverting the type system. I'll respond to more of your content when I'm confident I've understood you (which I don't mean as a brush off...).
    - comex 12y ago
      My response was poorly worded, but what I meant is that compilers for other languages with higher level type systems (which make more guarantees) cannot emit the same assembly as a C compiler, not that assembly is needed to subvert C's type system.
      - steveklabnik 12y ago
        Why not? Can you show me an example of what you mean? EDIT: I think the difference here is between 'types' and 'tags'. Types are at compile time. Tags are at runtime.

dkarapetyan 12y ago

Yes, type erasure is neat and a bit of thinking will make it obvious why proving static properties does not require run time checks if the transformations you perform on your program preserve those static properties. I disagree with the author's claim though that types are everywhere. Types in fact are extra structure that is hoisted onto programs. At the end of the day the machine knows nothing about the types and will shuttle bytes back and forth all day long. Furthermore, types restrict the universe of computation and there are examples of programs that are not well-typed but don't go wrong when evaluated.

mtdewcmu 12y ago
I wonder if type erasure is profound, or if it only sounds profound after being hypnotized by type theory.
- dkarapetyan 12y ago
  Don't get me wrong I think type theory is really cool. In fact any kind of theory that makes me a better programmer is cool. That's one of the reasons TypeScript right now is one of my favorite languages. It is the perfect balance between the prototyping power of dynamic languages and the awesome static guarantees of statically typed languages. The best part is that the type system does not get in the way when I'm prototyping and actually starts to help out when I have the design fleshed out. I just wish more languages supported that kind of type system because sometimes I really miss the static checks when writing stuff in Ruby and Python.
  - mtdewcmu 12y ago
    What I think is cool is getting computers to do things that are interesting. Types don't do anything. I find them hard to get excited about.
    - the_af 12y ago
      What do you mean "types don't do anything"? Are you seriously going to argue that? I don't know many people in the programming or CS fields who believe that. What some people believe is that there are type systems too onerous for the benefits they bring (which is, of course, debatable). Following your line of thought, one could say that the textual representation of your program "doesn't do anything" either, and neither does the syntax or the IDE/editor you use. So none of it matters. But of course it wouldn't be true -- all those things are useful tools that help you write software that does cool things. edit: thought of an even better example: tests. Tests "don't do anything". They are not directly related to the cool stuff we want to do with our computers. But who is going to argue that we shouldn't write any tests?

eudox 12y ago

The site is eerily similar to http://www.jonmsterling.com/index.html http://www.jonmsterling.com/index.html You two could hit it off or something.

dicroce 12y ago

If you were building a sandcastle, a type system is like plastic forms in the shape of castle components (walls, towers, etc)... They help you create a better sandcastle... This article was essentially saying: "You can remove the forms when you are done and your sandcastle will still stand."

taeric 12y ago
By that same analogy, building up a sand castle by only using those molds is a ridiculously hard way to build some castles.
- Lambdanaut 12y ago
  Fortunately some languages allow you to construct your own custom molds within the language itself.
  - taeric 12y ago
    Right, I was not trying to make an absolute "type systems are bad" statement. Just pointing out that the analogy can be used to cut both ways. :) Indeed, I think the analogy has pretty good legs. Consider, if you are working with cast iron, molds are the way to go.
  - aikah 12y ago
    and in others,one isnt even allowed to use his hands...
    - kazagistar 12y ago
      Your hands are your mind... you think the types, check the types, and erase them, but do all of it briefly, while playing with that part, and then move away. Compiled languages are like building a bunch of plaster mold, and then just doing the castle in one step. Optional typing, or using Any types and casting, is like using molds for a nice foundation, and using your hands to add little bits on top.

TheLoneWolfling 12y ago

Personally, I wish that type systems allowed for arbitrary pure (as in "same input -> same output") code to define what is and isn't a valid instance of a type at compile time. Being able to declare a function that is only valid for, say, power of two inputs (say: a hashmap's initial size, when the hashmap is using a bitwise and for wrapping) and having it actually enforced at compile time would be very useful. I mean, even range types are useful.

Ixiaus 12y ago
Dependent Types? Check out Idris.
- TheLoneWolfling 12y ago
  I shall have to. That being said, I don't care much for Haskell-based syntax.
  - saryant 12y ago
    Dotty is another option, a potential successor to Scala: https://github.com/lampepfl/dotty https://github.com/lampepfl/dotty
  - ixmatus 12y ago
    To each his own. I rarely hear fluent Haskellers say they don't care for the syntax though; if you haven't really gotten far enough to write production code in Haskell that leverages Haskell's powerful abstraction features, then you should and you might find the syntax growing on you. The syntax is nice because it enables the programmer to express software in a terse way, generally favoring the types as documentation and a strong mental model to understand the abstraction.
  - kazagistar 12y ago
    It is also a lot of work to prove your code. Here, have a nice Idris video to give you a taste: https://www.youtube.com/watch?v=P82dqVrS8ik https://www.youtube.com/watch?v=P82dqVrS8ik

TheLoneWolfling 12y ago

Isn't type erasure just a rather limited subclass of compiler optimization, and as such comes "for free" without having to explicitly code for it? The compiler frontend can leave in all type checks, having most of them can be removed by the optimizer, the same way you can remove any sort of redundant check (a default case in a switch statement over an enumeration, etc, etc) That being said, general type erasure can have (massive) problems. Look at Java.

lmm 12y ago
I'd say Java's type erasure has on the whole been massively successful (and it's allowed integration with e.g. Scala that a more reified type system might make difficult). What do you see as wrong with it?
- TheLoneWolfling 12y ago
  Too much wrestling with generics. For example, having to use a varargs hack just to make a T[] (that's an array of a a generic type). Or not being able to call T.class Or not being able to use instanceof T. Or having a Object[] that crashes at runtime when you try to put an Object in it. Or not being able to overload a method based on if it's passed a List<Foo> or List<Bar>. (Also applies to interfaces like Comparable, etc. There's no good way of going "this is a Comparable<Foo> and a Comparable<Bar>, but not a Comparable<Baz>.) Or for that matter, trying to pass an int[] to something that expects an Integer[], or vice versa. Or for that matter, someone passing in a List into your parameter expecting List<Foo> and crashing at runtime because it actually was a List<Bar>.
  - dgreensp 12y ago
    Java uses type erasure purely as a strategy for implementing generics. Combining type erasure and dispatch-on-type definitely produces some odd edges.
  - mcosta 12y ago
    It is ugly but you can make many of that things making all constructors request a paramter Class<T> cls. One thing you learn using java is not moving arrays around. The comparator stuff is true. Make the compiler to fail if you pass raw classes. A List is not a List<Foo> and in some cases is not a List<?> (where List is a class of <T extends Foo>). What I miss is some kind of self type, or "return this", I do not know how to tell it. Imagine a imaginary class A: this aMethod() { stuff(); return this; ) This aMethod returns an A when invoked on an A instance or a B, B extends A, if is a B instance. Handy for builders and fluid apis: B thisIsB = new B(); thisIsB.aMethod().bMethod();

juliangamble 12y ago

Some food for thought from Rich Hickey: "Statically typed programs and programmers can certainly be as correct about the outside world as any other program/programmers can, but the type system is irrelevant in that regard. The connection between the outside world and the premises will always be outside the scope of any type system." http://www.reddit.com/r/programming/comments/lirke/simple_made_easy_by_rich_hickey_video/c2u1fgc http://www.reddit.com/r/programming/comments/lirke/simple_ma...

Dewie 12y ago
I was more convinced by someone who replied to that post (psnively). He seems to be saying that type systems can't model the world as we know it perfectly, in which case it sounds like a Nirvana fallacy - we can model a lot of things that we care about as programmers, so even though we can't model all of it, it still has merit. If what he is referring to is that type systems are somehow "separate" from the outside world, then it seems somewhat like saying that mathematics is a wholly abstract field. Still, though, applied mathematics has been incredibly successful. After psnively's reply, Rich decides to throw a tantrum (read: "bow out").
gargantuan 12y ago
Also what about protocols? Can type systems handle that. Things like: * open file * close file * read form file That can be type checked up and down it will still be broken. Is that Rich Hickey meant? Here we are dealing with a real world -- a file. And it has a protocol to access it. So in a sense we want a protocol checker not a type checker in that case...?
- mcosta 12y ago
  I am pretty sure with a elaborate enough system with alias-forbidden types and resource managers you can do it. with file.open as f do .... alias = f // fail done // autoclose But then, is it really necessary?
- evincarofautumn 12y ago
  Separation logic can handle that—it’s a program logic that subsumes typechecking and typestate, among other things. Your example, in pseudocode: // open : string -> file_mode -> (f : file) | f @ read * f @ close f = open "input.dat" Read // close : (f : file) | f @ read * f @ close -> () close f // getline : (f : file) | f @ read -> string | f @ read s = getline f “open” grants the “read” and “close” permissions to “f”; “close” revokes the “read” permission that “getline” requires, causing “getline” not to typecheck.

pfh 12y ago

Types Are The Truth. Values Are The Proof.

CmonDev 12y ago

"Whether your programming language "embraces" types or has a modern type system or not, these concepts are central to how programs execute, because they are a fundamental part of how computation works." - what are "modern" type systems? Was something new invented in the last 15-20 years that I had missed?

todd8 12y ago

The discussion of types here is all over the place. This is because they are handled so differently in various programming languages. Pascal included array bounds in the type annotation for arrays and subscripting was enforced (at runtime) to be withing bounds. In C (and C++) arrays are almost equivalent to pointers (the full answer is complicated see [1]) and there is a real danger of buffer overflows. Python doesn't include type annotations, but the run-time enforces strong typing, lists carry their type information and will throw an exception if subjected to a non-list operation. The type system in Haskell is perhaps the best example of a really expressive and really effective system for ensuring that the compiler can catch as many error as possible at compile time. Haskell programmers sometimes say that if a program compiles it almost always works. This is interesting, but unfortunately, types and type annotations in use today don't fully capture the formal specification needed to guarantee program correctness. Just writing down specification in preparation for a proof of correctness can be difficult. The specifications have to be expressed in a formal system, for example some form of mathematical logic like predicate calculus. Working with anything less than a formal specification is like trying to solve a mathematical set of equations without using math symbols. Natural language is just inadequate to the task. See [2]. Getting the specifications right isn't easy. I remember my first attempt at proving the correctness of a sorting program. I understood that I needed to insure that A[i] <= A[i+1] for all elements in the array, but I forgot that the final result had to include all and only the original elements (i.e. that it had to be a strict permutation of the input elements). I don't believe that type systems are currently useful for these kind of specifications and verifications of program correctness. Real programs interact with the outside world (e.g. GUI's are hard to describe mathematically). Real programs often have distributed or concurrent execution for which new logics (like Temporal Logic) may have to be employed. Proving that a program will terminate or make progress or not deadlock or not livelock or will meet some real-time constraints are all exceptionally hard. Many years ago (in the 1980's) I worked on this research area at University. I had the hope that eventually, programming would be more like an interactive exploration with a sophisticated program prover. I thought that the programmer and software-prover would work together to produce a correct program. Today, we are still programming in pretty much the same old ways as back then. The languages are much better, but it's a harder problem than I thought it was going to be. [1] http://stackoverflow.com/questions/3959705/arrays-are-pointers http://stackoverflow.com/questions/3959705/arrays-are-pointe... [2] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD667.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/E...