Summer of Programming Languages(existentialtype.wordpress.com)
existentialtype.wordpress.com
Summer of Programming Languages
http://existentialtype.wordpress.com/2014/07/06/summer-of-programming-languages/
77 comments
These languages do have very theoretical foundations even though they might not be readily apparent. ML has a rich theory much of which is applicable to both Rust and Swift's type systems.
This is even more applicable to Rust where the system that deals with lifetimes and ownership are based on ideas that evolved out of linear/affine type systems that can track resource consumption.
Funnily enough linear type systems have a direct connection to linear logic, and via the Curry-Howard-Lambek there is another correspondence to symmetric/closed monoidial categories. Even though sometimes it appears like there is no theory behind these languages, Rust has definitely been aggressively importing some cutting edge thinking from programming languages.
This is even more applicable to Rust where the system that deals with lifetimes and ownership are based on ideas that evolved out of linear/affine type systems that can track resource consumption.
Funnily enough linear type systems have a direct connection to linear logic, and via the Curry-Howard-Lambek there is another correspondence to symmetric/closed monoidial categories. Even though sometimes it appears like there is no theory behind these languages, Rust has definitely been aggressively importing some cutting edge thinking from programming languages.
A language shouldn't need to have a foundation in category theory in order to be "grounded in theory and informed by practice."
I think that Bob's (the OP's) is merely saying that the design of languages such as Rust and Swift has been strongly influenced by developers well-versed in type theory (the foundation of programming languages) as well as software development (the point of programming languages) -- this is true for Haskell as well, as he points out, but he is just noting that these well-designed, informed languages are becoming more mainstream.
Also, Rust's type system is more complex than you might expect, involving something called linear/affine types: http://en.wikipedia.org/wiki/Substructural_type_system#Linea...
I think that Bob's (the OP's) is merely saying that the design of languages such as Rust and Swift has been strongly influenced by developers well-versed in type theory (the foundation of programming languages) as well as software development (the point of programming languages) -- this is true for Haskell as well, as he points out, but he is just noting that these well-designed, informed languages are becoming more mainstream.
Also, Rust's type system is more complex than you might expect, involving something called linear/affine types: http://en.wikipedia.org/wiki/Substructural_type_system#Linea...
I'd find it hard to justify nowadays understanding that there's a lot useful in Type theory but then ignoring Category theory. Even Object Orientation can be related to CT as coalgebras.
The type system in Haskell is not complex and that's a reason to like it. Everything derives from 6 simple rules:
http://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sys...
Simplicity in a type system makes it very expressive - contrast with complex, concrete type systems which do not allow e.g. Church numerals or linked lists to be represented within it.
The type system in Haskell is not complex and that's a reason to like it. Everything derives from 6 simple rules:
http://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sys...
Simplicity in a type system makes it very expressive - contrast with complex, concrete type systems which do not allow e.g. Church numerals or linked lists to be represented within it.
I recall reading that when Niko joined the Rust project, he kept uncovering places where the type system was unsound and was instrumental in making Rust type-safe. Can anyone confirm?
Well, we basically knew where the problems were, but Niko helped us come up with a way to fix them that was usable (the borrow check).
The language godfather and access to alternative languages for a given ecosystem play an higher role than how good a language might be.
Hence importance of having Apple and Microsost bringing ML derived languages into the industry.
Hence importance of having Apple and Microsost bringing ML derived languages into the industry.
> but none of these languages have much foundation in category theory or the ambitious kind of type system that Haskell has been pioneering for a while.
Is that a requirement? If so, why?
Is that a requirement? If so, why?
I've never seen a "bolt-on" type system work, and I've used a few (e.g. JSR308). So I think it's something that needs to be built into the language itself.
Having used a system with higher-level type constructs I find myself thinking in them. So many complex sequences of operations shake out as something much simpler once you realise the right monad, or arrow, or so on. And it becomes painful to manually expand it out; it would be like working in a language without generics. So I couldn't stand to work in a language that can't express these concepts; I need either higher-kinded types or something equivalent to them.
And for a type system that powerful, I'd want some assurance it was correct. Theoretical underpinnings are not the only way to do that - if it had been in use a while, and had enough tests and experience to give me a decent level of confidence, that would be enough. But for a new language I think the only way I could be confident enough to use it would be if it had this kind of theoretical backing.
Having used a system with higher-level type constructs I find myself thinking in them. So many complex sequences of operations shake out as something much simpler once you realise the right monad, or arrow, or so on. And it becomes painful to manually expand it out; it would be like working in a language without generics. So I couldn't stand to work in a language that can't express these concepts; I need either higher-kinded types or something equivalent to them.
And for a type system that powerful, I'd want some assurance it was correct. Theoretical underpinnings are not the only way to do that - if it had been in use a while, and had enough tests and experience to give me a decent level of confidence, that would be enough. But for a new language I think the only way I could be confident enough to use it would be if it had this kind of theoretical backing.
> I need either higher-kinded types or something equivalent to them.
FWIW it seems that many of the Rust developers want this for Rust.
FWIW it seems that many of the Rust developers want this for Rust.
Yes, many of us do. Using Option/Result can often lead to a lot of pain without their accompanying monads, and while you can write the specific ones (there's a try macro for using Option), it'd be much, much nicer to just have monads be possible in the language itself.
However, the Rust team is trying to get 1.0 out the door, and higher-kinded types would be backwards compatible, so I don't think we'll be seeing them for a while. There's also questions about the overhead and syntax that would need to be resolved for them to make it in.
However, the Rust team is trying to get 1.0 out the door, and higher-kinded types would be backwards compatible, so I don't think we'll be seeing them for a while. There's also questions about the overhead and syntax that would need to be resolved for them to make it in.
The backwards compatibility argument is interesting. I think it's really compelling, but it's also worth taking into account the pains that the Haskell community has been feeling since standardizing the standard library as insufficiently generic.
I have no idea if a similar problem is possible with Rust, but it'll be interesting to see how HKTs enter the scene if and when they do.
I have no idea if a similar problem is possible with Rust, but it'll be interesting to see how HKTs enter the scene if and when they do.
The Rust standard library will exist as an separate entity from the language itself, and can be versioned, updated, and deprecated just as any other library can, without being tied to any specific version of the language.
Bro, do you even liftM? ;)
For anyone who's interested in type theory and programming language foundations and modern development, I've found the talks of these summer schools really interesting and useful. The videos and material are at https://www.cs.uoregon.edu/research/summerschool/summer14/cu... , and you can change "14" in the URL to earlier years to see previous material. It's really a highly valuable set of resources.
Why do programming languages researchers seem so enamored with type-safe languages? It seems to be a given in academia that type-safe languages are not just superior, but significantly superior to type-unsafe languages.
It's a form of automation, which is, for understandable reasons, the most popular form of "progressive" PL thought. With a very powerful type system, the compiler can make inferences about the program that would otherwise be the programmer's burden. A powerful type system that is also safe allows whole classes of errors to either cease to exist, or be moved from runtime testing(where the programmer needs time and debugging skill to pinpoint their origin) to a compile-time error message. Either way, effort is saved each time the type system catches one of those errors.
Types are no silver bullet, however one important point missed by all the other replies is that static types check all paths through the program, including rare/untested/error paths.
You can sometimes make up for this with lots of testing and detailed code coverage analysis, but that can be a huge amount of effort, and might be impossible in some cases (for example: how do you easily test that your program behaves well when it runs out of disk space?). Static types can fix this with a lot less effort.
You can sometimes make up for this with lots of testing and detailed code coverage analysis, but that can be a huge amount of effort, and might be impossible in some cases (for example: how do you easily test that your program behaves well when it runs out of disk space?). Static types can fix this with a lot less effort.
There are cases you cannot really exclude by testing. For example, guaranteeing that certain function never receives a null value.
Sure you can! Just search exhaustively over your ultimately finite programs. There's a really simple algorithm for that, though the performance is a little wanting.
/s
(On a more serious sarcastic note, searching over your impure state space is somewhat more challenging. It's unclear how very finite it is, but I'm sure some reasonable spherical user assumptions will trim it to feasible exhaustiveness)
/s
(On a more serious sarcastic note, searching over your impure state space is somewhat more challenging. It's unclear how very finite it is, but I'm sure some reasonable spherical user assumptions will trim it to feasible exhaustiveness)
In Haskell, there isn't any null. The type-system ensures that a function can not receive a null value.
Functions can opt-in to the possibility of receiving 'Nothing' as a potential value. The tooling provided to Haskell can then also tell you when your function has not exhaustively handled every possible type of input (including Nothing).
In this instance, the type system provides robust automated coverage of your function's input domain w/regard to null values. Obviously type systems can't do everything, but they are the most light-weight formal methods we have.
Functions can opt-in to the possibility of receiving 'Nothing' as a potential value. The tooling provided to Haskell can then also tell you when your function has not exhaustively handled every possible type of input (including Nothing).
In this instance, the type system provides robust automated coverage of your function's input domain w/regard to null values. Obviously type systems can't do everything, but they are the most light-weight formal methods we have.
It is true that some things you just need to test, but nullability isn't actually one of them. Many languages—including SML, Haskell, Rust, and Swift—encode nullability in the type system, so those languages can guarantee at compile-time that functions never receive null values.
You read the comment backwards. It was saying exactly that nullability of the argument is something that can be guaranteed by a type system but you can't write a test that makes sure of it.
>Why do programming languages researchers seem so enamored with type-safe languages?
For the same reason people like unit tests. Only with mathematical rigor, checked by the compiler, and inspecting all aspects and code paths.
For the same reason people like unit tests. Only with mathematical rigor, checked by the compiler, and inspecting all aspects and code paths.
I agree that type-safe languages give a lot of the advantages of unit test.
I actually don't understand why those who advocate for TDD don't rather advocate you write everything in something like ATS. Every single argument I've seen for TDD would apply even more strongly to doing that.
I tried doing TDD style development for a while, and I found these two things to combine to make it unfeasible"
1) For significant amounts of real-world code writing correct tests is actually harder than writing correct code.
2) In real life you end up discarding much of the code you write.
This means that you end up spending a lot of extra effort to write well tested code that will never end up being run in production.
I find quality integration tests combined with some form of analysis of the more critical parts to be far more productive than TDD.
The equivalent for type-safe would perhaps be type-optional languages like Qi/Shen. I haven't messed around with it much, but it seems to offer rapid prototyping with an enforced type-safe mode that can be turned-on later. Unfortunately its inference engine seems to be inferior to ML or Haskell right now, so transforming code from non-typesafe to typesafe is a bit of a slog (I last tried it a year or two ago, so it may have improved in the meantime).
I actually don't understand why those who advocate for TDD don't rather advocate you write everything in something like ATS. Every single argument I've seen for TDD would apply even more strongly to doing that.
I tried doing TDD style development for a while, and I found these two things to combine to make it unfeasible"
1) For significant amounts of real-world code writing correct tests is actually harder than writing correct code.
2) In real life you end up discarding much of the code you write.
This means that you end up spending a lot of extra effort to write well tested code that will never end up being run in production.
I find quality integration tests combined with some form of analysis of the more critical parts to be far more productive than TDD.
The equivalent for type-safe would perhaps be type-optional languages like Qi/Shen. I haven't messed around with it much, but it seems to offer rapid prototyping with an enforced type-safe mode that can be turned-on later. Unfortunately its inference engine seems to be inferior to ML or Haskell right now, so transforming code from non-typesafe to typesafe is a bit of a slog (I last tried it a year or two ago, so it may have improved in the meantime).
Type-safe languages allow you to check the correctness of a program by proving a theorem about it: it will never suffer from implementation-defined, unspecified (by the language) behavior. Because of this property, programs written in a type-safe language have many more traces corresponding to the programmer's intention, by default, than programs written in unsafe languages. The tradeoff is that the programmer can have a harder time expressing his intentions.
In the case of Robert Harper in particular, see this blog post: http://existentialtype.wordpress.com/2011/03/19/dynamic-lang...
Meh, he's making a mathematical argument that dynamic languages are a special case of static languages. That has nothing to do with whether a language is good/productive for writing programs in.
I forget who said this, but programming language design is basically "applied psychology", and if you admit that, your language will go further. For example, the difference between Python and many similar languages is that it looks nicer and is "intuitive" to read, and that contributes a large part (perhaps the largest part) to its popularity.
I forget who said this, but programming language design is basically "applied psychology", and if you admit that, your language will go further. For example, the difference between Python and many similar languages is that it looks nicer and is "intuitive" to read, and that contributes a large part (perhaps the largest part) to its popularity.
There are also PL researcher who are enamored with dynamic languages. Alan Kay probably doesn't care much about static types.
Indeed, Gilad Bracha isn't a fan of static type systems.
Given that both Kay and Bracha are U if Utah PhDs, then it must be a Utah thing :) seriously, it is too easy to find lots of researchers on the dynamic side.
Types are the world's most popular verification technique. The whole intent of types is to automate many of the proofs required to guarantee the correctness of the program rather than having the human operator get bogged down in verifying the details themselves. Now yes, you can't verify all aspects of the program but types can still get you quite a distance of the way there at comparatively very little cost compared to more heavy formal verification techniques.
One of Harper's arguments (the author here) is dogmatic and perhaps compelling from a aesthetic point of view. Let me try not to butcher it too badly in what follows.
He believes a few things that in concert arrive at the idea that typed languages are the only interesting point in the design space thus uncovered.
He begins by first rigorously defining what he means by "type". In particular, it's a piece of information computed statically (i.e. using the syntax of a program alone, nothing of its "runtime") which constrains the eventual values the dynamics must take. A "type-safe" program is thus one where the dynamics correspond to the predictions of the statics—in particular, a program respects its type as it operates and the program "does not get stuck" i.e. does not hit an undefined state.
From here he notes the power of union types, types which are "either" A or B. Given a sufficiently large union type, one which reads "either this or that or this or that" for every possible result value of running a program then you can create a "safe" semantics for any language using this type—every program has this giant union type and every choice of dynamics ends up in this giant union type. He then notes that while this genuinely is "type safe" it's kind of boring. Further, all "dynamically typed" languages inherit this boringness since they expose no "interesting" static structure.
(Even if you dislike the argument above, and there's plenty that might cause someone to dislike it, it's worth noting that this line of thought arrives very smoothly at the concept of "hybrid typing" being explored by things like Typescript and Facebook's Hack.)
One of the primary things you could argue with at this point is that having more sophisticated types is interesting and valuable. To this end Harper focuses on what he calls the "Holy Trinity" of logic, type theory, and category theory. The idea is backed by the Curry-Howard-Lambek correspondence which shows that each of these fields is but an image of the other two. In Harper's (paraphrased) words: you know that something is genuine and lasting if you can show it exists in every branch of the Holy Trinity.
So he declares basically by fiat that things which reflect the Holy Trinity are interesting and things which do not are not. Obviously you can levy many arguments to disagree with him here.
But it's hard to declare that the things discovered in the Holy Trinity are boring. This is where cutting edge research on things like Homotopy Type Theory and general Dependent Types live. This produces compelling arguments to back up why "null pointers are a billion dollar mistake" [0] or why if-branching and booleans lack meaningful providence [1]. These ideas, even if they are stripped of their Ivory Tower gleam, are what are slowly percolating into mainstream languages with names like "Enum"++ in Swift and "Optional" in Java.
---
Generally, to finally provide my personal take, I think that Harper is dead right so long as you consider programming languages to be "means of expression". I think that's an interesting POV on languages generally and it's not totally at odds with the more everyday POV that languages are "tools for creation". But they are sometimes at odds since they place the brunt of what they demand of a language at different places. Ultimately, if Harper's program is successful many years from now we'll all use shadows of whatever futuristic grade of dependently typed language gives us maximal expressiveness while nesting it in an ecosystem of tooling and libraries which aid construction of interesting things. I have no idea if Harper's "one true language" exists, but it does seem like increasingly the world is moving that way... thus Harper's enthusiasm about Swift and Rust.
[0] http://qconlondon.com/london-2009/presentation/Null+Referenc...
[1] http://existentialtype.wordpress.com/2011/03/15/boolean-blin...
He believes a few things that in concert arrive at the idea that typed languages are the only interesting point in the design space thus uncovered.
He begins by first rigorously defining what he means by "type". In particular, it's a piece of information computed statically (i.e. using the syntax of a program alone, nothing of its "runtime") which constrains the eventual values the dynamics must take. A "type-safe" program is thus one where the dynamics correspond to the predictions of the statics—in particular, a program respects its type as it operates and the program "does not get stuck" i.e. does not hit an undefined state.
From here he notes the power of union types, types which are "either" A or B. Given a sufficiently large union type, one which reads "either this or that or this or that" for every possible result value of running a program then you can create a "safe" semantics for any language using this type—every program has this giant union type and every choice of dynamics ends up in this giant union type. He then notes that while this genuinely is "type safe" it's kind of boring. Further, all "dynamically typed" languages inherit this boringness since they expose no "interesting" static structure.
(Even if you dislike the argument above, and there's plenty that might cause someone to dislike it, it's worth noting that this line of thought arrives very smoothly at the concept of "hybrid typing" being explored by things like Typescript and Facebook's Hack.)
One of the primary things you could argue with at this point is that having more sophisticated types is interesting and valuable. To this end Harper focuses on what he calls the "Holy Trinity" of logic, type theory, and category theory. The idea is backed by the Curry-Howard-Lambek correspondence which shows that each of these fields is but an image of the other two. In Harper's (paraphrased) words: you know that something is genuine and lasting if you can show it exists in every branch of the Holy Trinity.
So he declares basically by fiat that things which reflect the Holy Trinity are interesting and things which do not are not. Obviously you can levy many arguments to disagree with him here.
But it's hard to declare that the things discovered in the Holy Trinity are boring. This is where cutting edge research on things like Homotopy Type Theory and general Dependent Types live. This produces compelling arguments to back up why "null pointers are a billion dollar mistake" [0] or why if-branching and booleans lack meaningful providence [1]. These ideas, even if they are stripped of their Ivory Tower gleam, are what are slowly percolating into mainstream languages with names like "Enum"++ in Swift and "Optional" in Java.
---
Generally, to finally provide my personal take, I think that Harper is dead right so long as you consider programming languages to be "means of expression". I think that's an interesting POV on languages generally and it's not totally at odds with the more everyday POV that languages are "tools for creation". But they are sometimes at odds since they place the brunt of what they demand of a language at different places. Ultimately, if Harper's program is successful many years from now we'll all use shadows of whatever futuristic grade of dependently typed language gives us maximal expressiveness while nesting it in an ecosystem of tooling and libraries which aid construction of interesting things. I have no idea if Harper's "one true language" exists, but it does seem like increasingly the world is moving that way... thus Harper's enthusiasm about Swift and Rust.
[0] http://qconlondon.com/london-2009/presentation/Null+Referenc...
[1] http://existentialtype.wordpress.com/2011/03/15/boolean-blin...
Thank you for this very well written and thoughtful response. It definitely answers some of my questions. I tend to come at problems from empirical and intuitive angles, so arguments from first-principles tend to be lost on me.
This is likely because my first encounter with formal reasoning was in the field of classical philosophy, and many things I empirically knew to be wrong had been "proven" from first-principles in the literature.
This is likely because my first encounter with formal reasoning was in the field of classical philosophy, and many things I empirically knew to be wrong had been "proven" from first-principles in the literature.
> Generally, to finally provide my personal take, I think that Harper is dead right so long as you consider programming languages to be "means of expression". I think that's an interesting POV on languages generally and it's not totally at odds with the more everyday POV that languages are "tools for creation".
That's a very concise way of putting it. My personal issue with a lot of what Harper writes is not that it's technically wrong per se, but it only makes sense if one is discussing programming languages purely from first principles. Harper seems really taken aback by the popularity of Haskell compared to SML in the functional programming space, and yet can't seem to wrap his head around the reason for the adoption is not so much about having ideal PL semantics but the fact Haskell has an industrial-strength cross-platform compiler with meaningful answers to modern problems ( FFI, concurrency, package management ). Haskell is rather unique in that it has a community that seems interested in building a language as both a "means of expression" and "tools for creation" and we've made some compromises between the two, no doubt. A lot of Harper's comments ( and many PL theorists ) seem to completely casually gloss over the gritty compiler engineering as if it's just beneath them, and that guys like SPJ and Simon Marlow are just wasting their time working on faster runtime systems and optimizations when he thinks they should be working on foundational "Holy Trinity" problems.
That's a very concise way of putting it. My personal issue with a lot of what Harper writes is not that it's technically wrong per se, but it only makes sense if one is discussing programming languages purely from first principles. Harper seems really taken aback by the popularity of Haskell compared to SML in the functional programming space, and yet can't seem to wrap his head around the reason for the adoption is not so much about having ideal PL semantics but the fact Haskell has an industrial-strength cross-platform compiler with meaningful answers to modern problems ( FFI, concurrency, package management ). Haskell is rather unique in that it has a community that seems interested in building a language as both a "means of expression" and "tools for creation" and we've made some compromises between the two, no doubt. A lot of Harper's comments ( and many PL theorists ) seem to completely casually gloss over the gritty compiler engineering as if it's just beneath them, and that guys like SPJ and Simon Marlow are just wasting their time working on faster runtime systems and optimizations when he thinks they should be working on foundational "Holy Trinity" problems.
> A lot of Harper's comments ( and many PL theorists ) seem to completely casually gloss over the gritty compiler engineering as if it's just beneath them, and that guys like SPJ and Simon Marlow are just wasting their time working on faster runtime systems and optimizations when he thinks they should be working on foundational "Holy Trinity" problems.
That's a tempting view to take regarding theory vs. practice but I don't think it holds up when you consider Harper's whole body of work and the substance of his criticisms of Haskell: He has published extensively on ML implementation and, as far as I know, has offered criticism of (GHC) Haskell's type system where it is unsound, never the (really cool) work being done on the RTS.
That's a tempting view to take regarding theory vs. practice but I don't think it holds up when you consider Harper's whole body of work and the substance of his criticisms of Haskell: He has published extensively on ML implementation and, as far as I know, has offered criticism of (GHC) Haskell's type system where it is unsound, never the (really cool) work being done on the RTS.
I've read his papers and I own his books, so I'm not entirely unfamiliar with his contributions to the field. But I also find his criticism of Haskell to be at best detached from reality and a "holistic" view of the programming profession as a union of theory, engineering, and community. Especially when he's arguing for the use of pure academic languages like Agda or antiquated ML-dialects that haven't seen active development in 15 years, over a productive language like Haskell. In an industry where regression languages like Go and Javascript are seeing wide adoption, I think his grandstanding does a lot more harm than good.
That makes sense. If you view Haskell as a research platform, pointing out ugly corners of the type system is entirely appropriate and even helpful for people working on GHC. From the outside, for those of us that would like to see these ideas gain greater adoption, it can be frustrating or even seem petty to focus on them.
It is helpful and appropriate to point out bugs, and his comments did help fix the Typeable exception problem in GHC 7.8. But he doesn't go through the usual tracker and mailing list to report these things. He goes off and writes these angry blog posts and extrapolates small defects to justify sensationalist claims about the whole language. On one hand you have a respected PL researcher, on another you have a guy who is like the axe-grinding "Zed Shaw" of functional languages.
Yes, this is what compelled me to comment in the first place: based on what I've read of his blog, that comparison (and his reputation in general) seems completely unjustified. There's a world of difference between this kind of spirited but productive debate and content-free holy wars between roughly identical languages that get the spotlight in the "mainstream" tech blog circuit.
In fact, his post on exceptions in Haskell and his criticism of monadic IO led me to work on some alternatives (algebraic effects) which, oddly enough, helped me understand Haskell's approach at a deeper level. I wouldn't have known about the issue if it was only on the bug tracker.
In fact, his post on exceptions in Haskell and his criticism of monadic IO led me to work on some alternatives (algebraic effects) which, oddly enough, helped me understand Haskell's approach at a deeper level. I wouldn't have known about the issue if it was only on the bug tracker.
I'm always reminded there's a long-tail to research. It's sad that so much focus goes to the peak of that distribution, though. I think the tension between useless and useful is really important!
Because designing type-safe languages is harder.
However, there is research into untyped/gradually typed languages. See, for example, [1] for combining gradual typing with type inference, and [2] for a list of papers formalizing the runtime semantics of a language that allows both typed and untyped functions.
[1] Gradual Typing with Unification-based Inference [2] http://homepages.inf.ed.ac.uk/wadler/topics/blame.html
However, there is research into untyped/gradually typed languages. See, for example, [1] for combining gradual typing with type inference, and [2] for a list of papers formalizing the runtime semantics of a language that allows both typed and untyped functions.
[1] Gradual Typing with Unification-based Inference [2] http://homepages.inf.ed.ac.uk/wadler/topics/blame.html
"Statically-typed" and "type-safe" don't mean the same thing.
"Type-safe" means that the type of a value is always correct. For example, if I have a function of type Int -> String, a type-safe language will not let me pass it a Float argument, no matter what I do. A type-unsafe language might let me, if I can "cast" the value to a new type without changing its representation (ie. it's still a Float, but the type-checker now thinks it's an Int).
Type-safe languages are preferred over type-unsafe languages, since they avoid all kinds of problems like undefined behaviour.
"Statically-typed" means that every variable, function argument, return value, etc. is associated with (usually one, "principle") type. These may be written explicitly, inferred, etc.
"Dynamically-typed" means that all values use the same static type. This type is usually a recursive sum of lots of useful types, for example (in pseudo-Haskell):
Many users of dynamically typed languages don't realise that static types are being used "behind the scenes", because:
* All of their code has the same type, so there's no need for any annotations, inference, type-checking or compilation. Many believe it's because there are no types, rather than the fact these have been made trivial.
* Sum types and recursive types aren't widely known, especially to those using dynamic languages who don't need to care about types at all. Hence, many make the assumption that "I don't know how to type this code" implies "this code is untypeable" and refer to such things as 'dynamic behaviour'.
* Many dynamic languages are implemented in languages with unsafe, anemic type systems, like C. Since 'dynamic behaviour' can't be represented safely in these languages, it's implemented unsafely, reinforcing the assumption that dynamic languages aren't type-safe.
* Other dynamic languages are implemented in themselves, which hides the UniType underlying it all.
* A few dynamic languages are implemented in languages with strong, safe type-systems, where the UniType is explicit and obvious, but most users stick to the dynamic language and never look at the implementation.
* Many languages confuse terminology by using the word "type" to refer to tags (the "I", "L", "F", "O", "E", ... in my UniType above); for example "if (get_type(x) === "int") {...}" instead of "if (get_tag(x) === I) {...}", but this doesn't make sense: types don't exist at runtime and even if they did the "get_type" function would always return the same thing (the UniType). The fact that many languages represent tags as strings doesn't help either!
* Dynamic languages allow any variable to contain any value, but most of the time only a small part of this domain is expected. This causes most functions to be partial, but whenever this partiality is encountered, one of two things happens: a) the program fails with a "runtime type error", which is incorrect and doesn't make sense, b) the language supplies an error value in response, and is regarded as doing something "unsafe" or "untyped", when in fact error values are perfectly valid (I've tagged them with "E" above) and it's the programmer's fault for not handling all of the possible cases they (implicitly, via UniType) asked for.
The work you've linked to is about selectively weakening the types in a program, so rather than having the whole thing be unityped or the whole thing use distinct types, instead we can write code both ways, then automatically strengthen/weaken the types and lower/lift the functions, so that they interoperate. The types are always safe, but the unityped part will have many more partial functions than total functions.
In contrast, we can't (yet) make a type system "gradually safe", since a single unsafe cast can break anything else ("ex falso quodlibet"). It would require some kind of para-consistent logic, which I've never seen in type theory. The difference is that 'gradual types' let us say "Any" instead of "Int", whereas unsafe types let us say "X" instead of "Int", for any "X".
"Type-safe" means that the type of a value is always correct. For example, if I have a function of type Int -> String, a type-safe language will not let me pass it a Float argument, no matter what I do. A type-unsafe language might let me, if I can "cast" the value to a new type without changing its representation (ie. it's still a Float, but the type-checker now thinks it's an Int).
Type-safe languages are preferred over type-unsafe languages, since they avoid all kinds of problems like undefined behaviour.
"Statically-typed" means that every variable, function argument, return value, etc. is associated with (usually one, "principle") type. These may be written explicitly, inferred, etc.
"Dynamically-typed" means that all values use the same static type. This type is usually a recursive sum of lots of useful types, for example (in pseudo-Haskell):
type UniType = I Int | L [UniType] | F (UniType -> UniType) | O (Object UniType) | E Error | ....
Many users of dynamically typed languages don't realise that static types are being used "behind the scenes", because:
* All of their code has the same type, so there's no need for any annotations, inference, type-checking or compilation. Many believe it's because there are no types, rather than the fact these have been made trivial.
* Sum types and recursive types aren't widely known, especially to those using dynamic languages who don't need to care about types at all. Hence, many make the assumption that "I don't know how to type this code" implies "this code is untypeable" and refer to such things as 'dynamic behaviour'.
* Many dynamic languages are implemented in languages with unsafe, anemic type systems, like C. Since 'dynamic behaviour' can't be represented safely in these languages, it's implemented unsafely, reinforcing the assumption that dynamic languages aren't type-safe.
* Other dynamic languages are implemented in themselves, which hides the UniType underlying it all.
* A few dynamic languages are implemented in languages with strong, safe type-systems, where the UniType is explicit and obvious, but most users stick to the dynamic language and never look at the implementation.
* Many languages confuse terminology by using the word "type" to refer to tags (the "I", "L", "F", "O", "E", ... in my UniType above); for example "if (get_type(x) === "int") {...}" instead of "if (get_tag(x) === I) {...}", but this doesn't make sense: types don't exist at runtime and even if they did the "get_type" function would always return the same thing (the UniType). The fact that many languages represent tags as strings doesn't help either!
* Dynamic languages allow any variable to contain any value, but most of the time only a small part of this domain is expected. This causes most functions to be partial, but whenever this partiality is encountered, one of two things happens: a) the program fails with a "runtime type error", which is incorrect and doesn't make sense, b) the language supplies an error value in response, and is regarded as doing something "unsafe" or "untyped", when in fact error values are perfectly valid (I've tagged them with "E" above) and it's the programmer's fault for not handling all of the possible cases they (implicitly, via UniType) asked for.
The work you've linked to is about selectively weakening the types in a program, so rather than having the whole thing be unityped or the whole thing use distinct types, instead we can write code both ways, then automatically strengthen/weaken the types and lower/lift the functions, so that they interoperate. The types are always safe, but the unityped part will have many more partial functions than total functions.
In contrast, we can't (yet) make a type system "gradually safe", since a single unsafe cast can break anything else ("ex falso quodlibet"). It would require some kind of para-consistent logic, which I've never seen in type theory. The difference is that 'gradual types' let us say "Any" instead of "Int", whereas unsafe types let us say "X" instead of "Int", for any "X".
Well, to people like Bob Harper, there is no such thing as a dynamic "type" (they are tags instead). The argument over terminology appears on comp.types every once in awhile. Then there are people into dynamic languages who swear they have more than one type and actually check these types at run type. Then the static type theorists say...you are just checking tags, and the DL people are like...what's the difference?
> DL people are like...what's the difference
The dynamic typing folks don't care to provide a definition of types and overload the term to mean many things, the static typing folks have a rigorous one.
The dynamic typing folks don't care to provide a definition of types and overload the term to mean many things, the static typing folks have a rigorous one.
[deleted]
I see no definitions of type in the dictionary that specifically refer to static type theory...
Definition of type (n)
category or kind: a group made up of individuals or items that have strongly marked and readily defined similarities
person or thing: somebody or something regarded as belonging to a group or category by virtue of having the main qualities associated with it
particular kind of person: a person regarded as having a particular temperament or characteristics.
Definition of type (n)
category or kind: a group made up of individuals or items that have strongly marked and readily defined similarities
person or thing: somebody or something regarded as belonging to a group or category by virtue of having the main qualities associated with it
particular kind of person: a person regarded as having a particular temperament or characteristics.
It's a technical term so the colloquial definition has little relevance to it's use in computing. You can read the definition in TAPL or PFPL.
> tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
> tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
Type is pretty much used by most programmers to mean "type" as it is stated in the dictionary; so dynamic type checking is not a misnomer to them. Only type theorists are diligent about the colloquial definition, but they can only really use it like that when talking to other type theorists.
Well, if the other person doesn't at least understand that much, speaking to them is probably a waste of time anyway.
Yes, perhaps type theorists are best talking to other type theorists and not people who actually program.
Agree.
> It's a technical term so the colloquial definition has little relevance to it's use in computing. You can read the definition in TAPL or PFPL.
Technical books often define terms in a way convenient for the material and approach they are presenting, not in a way that is general to the field; particularly, if terms are used in different ways within the field at the time they are written, they typically have to choose for consistency within the book -- that doesn't make that definition the right one for the field, it simply means that's what the term means in the context of the work.
And, ultimately, the semantic argument is meaningless. It doesn't really matter whether you have static and dynamic types in different languages or you call the former "types" and the latter "tags" (except that the former terminology actually explains the difference in a way that tells you what the difference is every time you use the terms.) The substance is the same, and getting worked up over line-drawing regarding the boundary of "type" is a distraction from any discussion of substance.
Technical books often define terms in a way convenient for the material and approach they are presenting, not in a way that is general to the field; particularly, if terms are used in different ways within the field at the time they are written, they typically have to choose for consistency within the book -- that doesn't make that definition the right one for the field, it simply means that's what the term means in the context of the work.
And, ultimately, the semantic argument is meaningless. It doesn't really matter whether you have static and dynamic types in different languages or you call the former "types" and the latter "tags" (except that the former terminology actually explains the difference in a way that tells you what the difference is every time you use the terms.) The substance is the same, and getting worked up over line-drawing regarding the boundary of "type" is a distraction from any discussion of substance.
Yes, the usage of the word "type" depends on the community; I would say it's not controversial to use the type-theoretic context here, since TFA is written by a type theorist.
However, my main point was that "type-safe" and "type-unsafe" are not synonimous with "static" and "dynamic". The original question was probably about static vs dynamic, but I think it's important to point out the distinction; especially when reading material like Bob's that assumes some familiarity with the terms.
From a Curry-Howard point of view:
* Static types are logical formulas, values are their proofs.
* "Dynamic types" are the clauses of one big disjunctive formula: Int OR Bool OR Error OR Array OR String OR ....
* Safe type systems are sound logics; they don't let us prove "FALSE".
* Unsafe type systems are unsound logics; they let us prove "FALSE", and hence anything (ex falso quodlibet).
Importantly, the big disjunctive formula used by dynamic languages is trivial to prove. For example, I can prove it with a constant like "10", without having to perform any computation. Trivial formulas are equivalent to "TRUE" (the logical proposition, not the boolean value!), hence dynamic languages only allow us to prove "TRUE". This makes them type-safe, since they can't prove "FALSE", but it makes them uninformative: proving "TRUE" doesn't tell us anything we didn't already know!
The only languages which can be type-unsafe are static languages, since they're the only ones which can express types other than "TRUE" (eg. "FALSE"). If a static language is unsafe, then there's essentially no benefit to it having static types, since we can't trust any of the information it gives us.
That's why academics prefer type-safe languages, whether they're static or dynamic, whether or not you agree with Harper that one's a sub-set of the other. Unsafe languages specifically hinder our reasoning. Sure, we might be confident that our particular C program is safe, despite C being an unsafe language, but we can't generalise that to "for all C programs 'P'...", which makes it difficult to study languages-in-the-abstract. Of course, we lose nothing if we make the language safe, so we might as well do that (eg. define a safe sub-set of C like http://compcert.inria.fr/doc/ ).
Essentially, asking "Why do programming languages researchers seem so enamored with type-safe languages?" is like asking "Why do Mathematicians seem so enamored with sound logics?". Of course, there is research in non-monotonic logics, para-consistent logics, etc. and that's great, but if we're going to have an academia-vs-industry debate, then I think the unsound logics, and hence the type-unsafe languages, have the taller ivory towers.
Of course, there are many other ways that static and dynamic languages may be safe or unsafe (eg. memory safety, thread safety, non-total, etc.). (Safe) type systems can eliminate some of these problems (eg. memory safety with linear types), but just because it's possible with some type-system feature doesn't make a language lacking that feature type-unsafe; the worst we could say is that it's type-uninformative.
For example, Haskell's type system doesn't distinguish total functions (eg. via a data/codata separation). This makes Haskell unsafe with regards to termination/cotermination, but it doesn't make Haskell type-unsafe. Since dynamic types are completely uninformative, they can't solve any problems that type systems are suited to, but that still doesn't make them type-unsafe.
For example, it's not that dynamic languages allow type-unsafe operations like passing strings to "+ : Int -> Int -> Int", it's that dynamic languages don't allow us to restrict the type of "+" at all; we can't even specify that it's a function, let alone what that function's input and return types are! If it generates a run-time error that's fine, since "run-time error" is a perfectly valid value, as far as the type system's concerned.
Now, we may think this is an unsafe thing to do, but it doesn't make the language type-unsafe. It just makes it "semantically unsafe" or "unsafe without lots of tests" or somesuch.
However, my main point was that "type-safe" and "type-unsafe" are not synonimous with "static" and "dynamic". The original question was probably about static vs dynamic, but I think it's important to point out the distinction; especially when reading material like Bob's that assumes some familiarity with the terms.
From a Curry-Howard point of view:
* Static types are logical formulas, values are their proofs.
* "Dynamic types" are the clauses of one big disjunctive formula: Int OR Bool OR Error OR Array OR String OR ....
* Safe type systems are sound logics; they don't let us prove "FALSE".
* Unsafe type systems are unsound logics; they let us prove "FALSE", and hence anything (ex falso quodlibet).
Importantly, the big disjunctive formula used by dynamic languages is trivial to prove. For example, I can prove it with a constant like "10", without having to perform any computation. Trivial formulas are equivalent to "TRUE" (the logical proposition, not the boolean value!), hence dynamic languages only allow us to prove "TRUE". This makes them type-safe, since they can't prove "FALSE", but it makes them uninformative: proving "TRUE" doesn't tell us anything we didn't already know!
The only languages which can be type-unsafe are static languages, since they're the only ones which can express types other than "TRUE" (eg. "FALSE"). If a static language is unsafe, then there's essentially no benefit to it having static types, since we can't trust any of the information it gives us.
That's why academics prefer type-safe languages, whether they're static or dynamic, whether or not you agree with Harper that one's a sub-set of the other. Unsafe languages specifically hinder our reasoning. Sure, we might be confident that our particular C program is safe, despite C being an unsafe language, but we can't generalise that to "for all C programs 'P'...", which makes it difficult to study languages-in-the-abstract. Of course, we lose nothing if we make the language safe, so we might as well do that (eg. define a safe sub-set of C like http://compcert.inria.fr/doc/ ).
Essentially, asking "Why do programming languages researchers seem so enamored with type-safe languages?" is like asking "Why do Mathematicians seem so enamored with sound logics?". Of course, there is research in non-monotonic logics, para-consistent logics, etc. and that's great, but if we're going to have an academia-vs-industry debate, then I think the unsound logics, and hence the type-unsafe languages, have the taller ivory towers.
Of course, there are many other ways that static and dynamic languages may be safe or unsafe (eg. memory safety, thread safety, non-total, etc.). (Safe) type systems can eliminate some of these problems (eg. memory safety with linear types), but just because it's possible with some type-system feature doesn't make a language lacking that feature type-unsafe; the worst we could say is that it's type-uninformative.
For example, Haskell's type system doesn't distinguish total functions (eg. via a data/codata separation). This makes Haskell unsafe with regards to termination/cotermination, but it doesn't make Haskell type-unsafe. Since dynamic types are completely uninformative, they can't solve any problems that type systems are suited to, but that still doesn't make them type-unsafe.
For example, it's not that dynamic languages allow type-unsafe operations like passing strings to "+ : Int -> Int -> Int", it's that dynamic languages don't allow us to restrict the type of "+" at all; we can't even specify that it's a function, let alone what that function's input and return types are! If it generates a run-time error that's fine, since "run-time error" is a perfectly valid value, as far as the type system's concerned.
Now, we may think this is an unsafe thing to do, but it doesn't make the language type-unsafe. It just makes it "semantically unsafe" or "unsafe without lots of tests" or somesuch.
Academics don't care so much about things like programming speed. And the academic environment focusses on proof; a type-safety property will seem much better than a unit test even when both took the same amount of time and have the same practical value.
(For all that, I agree with them though. Maybe the reason programming languages researchers think that is because it's true? Do you have reason to believe they're wrong?)
(For all that, I agree with them though. Maybe the reason programming languages researchers think that is because it's true? Do you have reason to believe they're wrong?)
My experience with unit tests for dynamic languages as a replacement for proper static typing done at the compiler level, is that it just doesn't work.
Sure it works for the lonely coder or small shops, but as soon as the project scale increases anything goes.
Managers will push for features over unit tests, no one will refactor code without taking a few days with the caveat not all places will be touched and the team atrition will bring in new devolpers forced to read implementation code to be sure how to properly call the functions/methods.
Advanced static typed languages with HM type inference are a better option for large scale development.
Hence it may be that is harder to get funding for other types of research.
Other issue is that dynamic languages fo their very nature make tooling harder problem to solve, hence less interesting for many researchers, pressed with delivering quick results.
Sure it works for the lonely coder or small shops, but as soon as the project scale increases anything goes.
Managers will push for features over unit tests, no one will refactor code without taking a few days with the caveat not all places will be touched and the team atrition will bring in new devolpers forced to read implementation code to be sure how to properly call the functions/methods.
Advanced static typed languages with HM type inference are a better option for large scale development.
Hence it may be that is harder to get funding for other types of research.
Other issue is that dynamic languages fo their very nature make tooling harder problem to solve, hence less interesting for many researchers, pressed with delivering quick results.
I don't necessarily think they are wrong, but I also think that (as with most "silver bullets") type-safety is not without it's shortcomings.
For example, consider the exponentiation function. When we raise an Integer to a positive Integer (2^2), the result will always be a positive Integer. You would expect the type of such a function to be: Integer -> Integer -> Integer
Except, that's wrong. When we raise an Integer to a negative Integer (2^-2), the result will be some fractional value. If we want to retain full numeric precision, it'll have to be something like a Rational. So now your function's type signature is: Integer -> Integer -> Rational.
But that's also wrong. So what are we to do? Maybe positive and negative integers should be separate types? PositiveInt and NegativeInt, let's say. But then what about subtraction? Should it's type signature be: PositiveInt -> PositiveInt -> PositiveInt? What about 2 - 3? Whoops!
So, there's no way, with types alone, to simply and accurately encode all basic math operations. All you can do is throw a Domain Error when someone violates certain boundary conditions, and tell them to check their arguments before deciding which function to call.
...meanwhile, dynamic languages will happily return whatever type is most appropriate for the arguments given.
For example, consider the exponentiation function. When we raise an Integer to a positive Integer (2^2), the result will always be a positive Integer. You would expect the type of such a function to be: Integer -> Integer -> Integer
Except, that's wrong. When we raise an Integer to a negative Integer (2^-2), the result will be some fractional value. If we want to retain full numeric precision, it'll have to be something like a Rational. So now your function's type signature is: Integer -> Integer -> Rational.
But that's also wrong. So what are we to do? Maybe positive and negative integers should be separate types? PositiveInt and NegativeInt, let's say. But then what about subtraction? Should it's type signature be: PositiveInt -> PositiveInt -> PositiveInt? What about 2 - 3? Whoops!
So, there's no way, with types alone, to simply and accurately encode all basic math operations. All you can do is throw a Domain Error when someone violates certain boundary conditions, and tell them to check their arguments before deciding which function to call.
...meanwhile, dynamic languages will happily return whatever type is most appropriate for the arguments given.
Any property that you can actually be confident about, you can encode into the type system. If you care that x ^ (y - z) is an integer, you'd better have some reason to believe that y > z. If you don't care or can't be sure, let x ^ (y - z) return Integer | Rational, and pattern-match for the cases (or treat them as some supertype, Numeric or some such). Or if you really can't figure out the proof but still think it's correct, you can cast, and then your program will error out at runtime if you're wrong, which is at least safe.
In a dynamic language, your mistake passes silently; the result you thought was an integer is actually a fraction, but your program carries on going. Maybe it turns it into a string and uses it as a file path, so something you thought was a simple filename has a slash in it. Maybe that breaks your security model. Pretty unlikely in this specific case, but that's how bugs happen.
In a dynamic language, your mistake passes silently; the result you thought was an integer is actually a fraction, but your program carries on going. Maybe it turns it into a string and uses it as a file path, so something you thought was a simple filename has a slash in it. Maybe that breaks your security model. Pretty unlikely in this specific case, but that's how bugs happen.
Right, but it's also much simpler and faster for the programmer to write one function with one return type, and later modify it to add a return type if the requirements change. I think this is obviously why dynamic languages rose in prominence coincidentally with the rise in rapid prototyping and agile development. That said, this is also why large companies with codebases that need to be maintained over multiple decades will always go with static languages.
What really interests me are languages like Julia or Dart, with their gradual typing, or Clojure and core.typed. You retain the flexibility and speed of development of a dynamic language, with the possibility of later adding type safety guarantees to your code without having to rewrite it from scratch.
What really interests me are languages like Julia or Dart, with their gradual typing, or Clojure and core.typed. You retain the flexibility and speed of development of a dynamic language, with the possibility of later adding type safety guarantees to your code without having to rewrite it from scratch.
> it's also much simpler and faster for the programmer to write one function with one return type, and later modify it to add a return type if the requirements change.
How is this different? When you compile, your compiler will say "Hey, the requirements have changed, your code is wrong here, here, here, and here," and you modify those things, and you're done.
How is this different? When you compile, your compiler will say "Hey, the requirements have changed, your code is wrong here, here, here, and here," and you modify those things, and you're done.
....and then you've forgot what you were actually trying to solve.
What is the alternative? You change the code, the behavior gets changed but the compiler doesn't warn you. At this point you have two possible paths:
1- You wrote tests which start failing. You must now spend time changing them. You don't manage to avoid working in order fix your safety net (be it static type checking or your test suite).
2- You didn't write the right tests, and don't notice the change in behavior. The program later fails in production.
1- You wrote tests which start failing. You must now spend time changing them. You don't manage to avoid working in order fix your safety net (be it static type checking or your test suite).
2- You didn't write the right tests, and don't notice the change in behavior. The program later fails in production.
Why? Aren't you trying to solve the change in interface? And wouldn't you be making the same changes in a dynamically typed language?
I find the type system a great help with remembering what I was actually trying to solve. I can "start at the end" and then work backwards, solving one compile error at a time until there aren't any left, at which point I'll know I've done what I wanted to.
> Any property that you can actually be confident about, you can encode into the type system.
The big theoretical drawback is that you get an unbounded increase in program length. The reason is that programs in a typed language are proofs, and proof length cannot be bounded above by any computable function of proposition length.
The big practical drawback is that we just don't know how to explain proofs to a computer very well.
The big theoretical drawback is that you get an unbounded increase in program length. The reason is that programs in a typed language are proofs, and proof length cannot be bounded above by any computable function of proposition length.
The big practical drawback is that we just don't know how to explain proofs to a computer very well.
It turns out that it's quite possible to express almost all of the invariants you describe in a type system, and we've done it in Typed Racket. Vincent St-Amour wrote a paper about it: http://www.ccs.neu.edu/racket/pubs/padl12-stff.pdf
It can express that 2^2 is positive and an integer, that 2^-2 is positive and a rational, and that 2-3 is an integer but not necessarily positive.
It can express that 2^2 is positive and an integer, that 2^-2 is positive and a rational, and that 2-3 is an integer but not necessarily positive.
>Academics don't care so much about things like programming speed.
I don't know. Haskell and OccamL, for one, are much, much faster than Python and Ruby.
I don't know. Haskell and OccamL, for one, are much, much faster than Python and Ruby.
Citation needed. The argument for Haskell is usually about correctness; industry perception and my experience is that writing a Haskell version of a program will usually take longer than an "acceptably buggy" Python or Ruby equivalent.
Well, there's the 1994 US Navy experiment that shows Haskell is a serious contender for rapid prototyping: http://cpsc.yale.edu/sites/default/files/files/tr1049.pdf
Of course, there was no Ruby back then. The comparison was against C++, Ada, Awk (!?), something called "relational Lisp" and a variety of in-house languages. Haskell comes just after Lisp in development time, with a mind-boggling 8 hours! (No C++ times were reported... heh heh). The Haskell solution also got top marks in general, not just in development time. As a downside, some of the reviewers didn't understand it because they weren't well-versed in functional programming, and felt some of the Haskell code was "tricky".
Of course, there was no Ruby back then. The comparison was against C++, Ada, Awk (!?), something called "relational Lisp" and a variety of in-house languages. Haskell comes just after Lisp in development time, with a mind-boggling 8 hours! (No C++ times were reported... heh heh). The Haskell solution also got top marks in general, not just in development time. As a downside, some of the reviewers didn't understand it because they weren't well-versed in functional programming, and felt some of the Haskell code was "tricky".
[deleted](1)
I would say its because academic researchers don't spend nearly enough time actually using these languages industriously in the worst-case scenarios. If more effort was spent in understanding how, for example, SIL-4 (safety integrity level 4) development is done with non-type-safe languages (hint: code coverage tests, tests, tests..), then there would (imho) be less motivation to continually churn out 'new solutions to old problems' .. which have been solved, already.
Fact is, if you can't trust your language because of its type system, you develop tools to build that trust around your particular application of the language. If that is 'too much work for you' .. then by all means, avoid the work by reinventing the wheel. In Academia, you can get away with that because you don't have customers, and you don't have an industry demanding results. At most you have peers whom you have convince that steering their groupthink in your direction is worth the effort.
Fact is, if you can't trust your language because of its type system, you develop tools to build that trust around your particular application of the language. If that is 'too much work for you' .. then by all means, avoid the work by reinventing the wheel. In Academia, you can get away with that because you don't have customers, and you don't have an industry demanding results. At most you have peers whom you have convince that steering their groupthink in your direction is worth the effort.
>* If more effort was spent in understanding how, for example, SIL-4 (safety integrity level 4) development is done with non-type-safe languages (hint: code coverage tests, tests, tests..), then there would (imho) be less motivation to continually churn out 'new solutions to old problems' .. which have been solved, already.*
Because ad-hoc tests, tests, tests, ... with the verbosity they add (tons of uneeded tests that could be type checked instead), and the arbitrariness (you have to remember to add a test -- instead type checks are always run) and checking only some code paths (type checks propagate everywhere) are in any way better?
Not to mention that you can have type checks AND (less, complimentary) tests at the same time.
Because ad-hoc tests, tests, tests, ... with the verbosity they add (tons of uneeded tests that could be type checked instead), and the arbitrariness (you have to remember to add a test -- instead type checks are always run) and checking only some code paths (type checks propagate everywhere) are in any way better?
Not to mention that you can have type checks AND (less, complimentary) tests at the same time.
Let's just say that the attitude of IEC 61508 towards software development in general and programming languages in particular is not very spirit-lifting.
At least us software guys have an advantage: the hardware guys will always have to live with failure rates.
But the standard happily declares software to be bug-free, as long as you do the required testing and stuff. ;-)
At least us software guys have an advantage: the hardware guys will always have to live with failure rates.
But the standard happily declares software to be bug-free, as long as you do the required testing and stuff. ;-)
"Fact is, if you can't trust your language because of its type system, you develop tools to build that trust around your particular application of the language. If that is 'too much work for you' .. then by all means, avoid the work by reinventing the wheel."
But aren't those tools (that can build trust) something that could be built-in & available to all users of the language, therefore avoiding "reinventing the wheel"? Why would you want to do by hand something that can be automated?
But aren't those tools (that can build trust) something that could be built-in & available to all users of the language, therefore avoiding "reinventing the wheel"? Why would you want to do by hand something that can be automated?
[deleted]
Any ideas why software verification videos are not published in the OPLSS web page?
This seems a bit overly optimistic, but it's nice to see this kind of positive attitude for a change instead of "Why invent yet another language?".
I am very excited about Swift and I have some respect for what Rust is trying to accomplish, but none of these languages have much foundation in category theory or the ambitious kind of type system that Haskell has been pioneering for a while. And the fact that Go is seeing some traction is a stark reminder that we still have ways to go.
Still, it's nice to see some of these concepts becoming mainstream (lambdas/closures, fold and functional iteration, phasing off inheritance based polymorphism, etc...).