10 ms·

Type systems and the future of programming languages

74 points by lewisjoe 7y ago

azhenley 7y ago
Anyone know who wrote this?
- fauigerzigerk 7y ago
  I don't know, but I wouldn't be surprised if he did: https://github.com/joelewis https://github.com/joelewis
karmakaze 7y ago
What's the purpose of posting as a G-Doc instead of HTML? The visitors' google account info could potentially be collected.
- 3pt14159 7y ago
  Not really anymore. It's now anonymized by default.
  - nixpulvis 7y ago
    Color me skeptical. Plus it breaks the "visited" styling on HN, and generally pisses me off for throwing me out of my browser. <angry old man waves fist at cloud />
- BLanen 7y ago
  Or just a pdf uploaded to wherever. Even google Drive.
malkia 7y ago
The webpage for AGDA seems to be https://github.com/agda/agda https://github.com/agda/agda or https://wiki.portal.chalmers.se/agda/pmwiki.php https://wiki.portal.chalmers.se/agda/pmwiki.php, but not https://www.agda.com.au/ https://www.agda.com.au/ (end of the paper).
- lewisjoe 7y ago
  Thanks. Fixed the links.
lidHanteyk 7y ago
I'd like to joke that we could replace the link with [0] and it would be a massive improvement. Seriously, though, these descriptions of type-theoretic programming as a solution to a problem, rather than a tower to be climbed, are increasingly obscurantist, hiding the meat of the correspondence behind analogies and narratives. [0] https://ncatlab.org/nlab/show/computational+trinitarianism https://ncatlab.org/nlab/show/computational+trinitarianism
- carapace 7y ago
  > hiding the meat of the correspondence behind analogies and narratives. Interesting. Could you elaborate a little?
  - lidHanteyk 7y ago
    Sure. Any time somebody says "Curry-Howard" and doesn't provide the table that I provided, they are handwaving. The table makes the correspondence precise.
    - carapace 7y ago
      Cheers. When you say "the correspondence behind analogies and narratives", which column is analogy and which is narrative? I hope I'm not being really dense or ignorant here, apologies if so.
      - lidHanteyk 7y ago
        The page I linked is relatively clear. I was complaining about the original article, which fails to make contact with the actual guts of formal type theory.
        carapace 7y ago
        Right, I get that. But the words "analogy" and "narrative" don't appear in the page. I'm wondering what you mean by those words?
abeppu 7y ago
This author predicts that we'll drift towards languages like Agda or Idris, and also discusses how type systems came out of math. I'm curious about two related questions: 1. Why is it that a minority of math is done with proof systems (i.e. yielding automatically checkable artifacts)? It's burdensome to formalize much of the math that we're interested, even when we're confident in that math. What's the nature of that burden, and how could tools improve to lessen it? 2. Are the difficulties which prevent a lot of math from being done with these systems the same as the difficulties which prevent programmers from using them? There are many invariants that we can easily know about a program, but representing the lot of them in types would be onerous. How do we make that easier/lighter?
- zozbot234 7y ago
  > Why is it that a minority of math is done with proof systems (i.e. yielding automatically checkable artifacts)? Because most interesting math depends on a lot of other math, and formalizing all of these pre-requirements is a significant burden. The math subfields where this is less of a problem (so-called 'synthetic' mathematics) are also where formalization is being used the most.
  - Smaug123 7y ago
    And additionally it takes a lot of effort to formalise a proof. (I say this as someone who has spent nearly two years formalising basic maths in Agda.) It's true in maths as in programming: 90% of the work is in the last 10%, and if you don't get the last 10%, you haven't got a proof.
    - zozbot234 7y ago
      The usual rule of thumb is that 1 page of paper proof leads to 4 pages of "proper" formal proof. Though this may vary depending on how capable the proof assistant is - AIUI, Agda requires you to write out complete proof terms, whereas other systems may be more capable. Sometimes you can use a kind of "reflection" that makes many proofs trivial, simply by defining a decision procedure that's proven to be correct in the general case, and having the system perform the appropriate computations. This is how you would deal, e.g. with trivial simplifications in elementary algebra (that can usually be proven to be valid in any ring, field etc.)
pcwalton 7y ago
We aren't going to move to dependently-typed languages based around theorem proving anytime soon. The reason is simple: those languages don't support normal industry development practices, where you don't have time to spend 10x the time on verification as you do on development. (They do support development practices favored by the US Department of Defense, which is perhaps part of the reason why research into such type systems attracts DARPA grants.) Where such languages may have a future is for proving some kernel of core infrastructure code correct, where the code has such a high value to size ratio that spending the time to prove it correct may cross the line into economic viability. SeL4 is a high-profile example of this. Another example that's been on my mind over the years could be proving the unsafe code in the Rust standard library correct. The latter would be interesting because it would address the criticism of "well, there's unsafe code in libstd, how can you say Rust is safe?" without burdening regular Rust users (not standard library developers) with all the baggage of a complex type system.
- zozbot234 7y ago
  > The reason is simple: those languages don't support normal industry development practices, where you don't have time to spend 10x the time on verification as you do on development. In practice, these languages have good support for gradual development so no, you don't have to spend 10x your dev time on verification. You can focus your verification effort on the lowest-hanging fruit, such as properties that only depend on local reasoning, as opposed to non-trivial interactions involving the program as a whole. (One potential issue for this is that dependently-typed languages are total languages, so any code that's 'natively' written in the languages must be proven to terminate. But partiality and Turing-completeness can be reintroduced in a fairly trivial way by resorting to a 'Delay' or 'Partial' monad.)
- phillipcarter 7y ago
  There’s also the problem where inferring the types is not decidable, so we either get slow tooling/builds or an onerous development cycle of specifying everything. The latter would be unbearable when you consider how weird and annoying things relate to one another in large, enterprisey systems.
smitty1e 7y ago
What I'd like to locate/implement would be: - an in-memory SQLite database with - a sufficiently generalized schema that could - ingest the static type information emitted by, say GCC, so that - one could easily inspect/compare metadata from any language. I doubt that this idea is unique to me.
- Boulth 7y ago
  Sounds like Language Server: https://langserver.org/ https://langserver.org/
  - smitty1e 7y ago
    Same idea carried further to include data types and objects that actual programs in the languages use, not just the EBNF grammar constructs of the languages. Unless I missed that in my quick glance at the link.
    - Boulth 7y ago
      Yep, LSP does include semantic view of the code. That is anything you'd see at the end tools such as IDEs: types, members, functions, properties within context (e.g. this function is a member of this class).
- oscargrouch 7y ago
  If im not mistaken, what you want is basically this: https://kythe.io/ https://kythe.io/ Also lets not forget that LLDB can basically be that (at least for LLVM languages) https://lldb.llvm.org/resources/architecture.html https://lldb.llvm.org/resources/architecture.html "LLDB converts debug information into Clang types so that it can leverage the Clang compiler infrastructure. This allows LLDB to support the latest C, C++, Objective-C and Objective-C++ language features and runtimes in expressions without having to reimplement any of this functionality." By the way, Visual Studio and Code with the C++ plugin is using the embedded version of SQL Server database.. so they probably have this sort of architecture, for index, debugging, etc.. So somewhere they might at least decribe how they (Microsoft) are doing this in Visual Studio architecture.
crimsonalucard 7y ago
LEAN is another popular language in this area. There are huge benefits for moving the industry in this direction. Such programs that are formally correct eliminates the need for testing almost completely and can cut such infrastructure down by possibly 95%. A program can use dependent typing to prove itself 100% correct vs. 100 unit tests which proves only 100 arbitrary test cases as correct. Unit tests are statistical experiments where the people hope that the verification of 100 arbitrary test cases correlates with the entire program being correct. Yes, proofs are harder to write than tests, yes there can be bugs in your proof (their can be bugs in tests too). However, I genuinely believe that for the lifetime of an application, in general, the net benefits of dependent types is positive and greater than that provided by testing. However I do not believe the industry will move in this direction. The reason why the industry won't move in this direction is largely cultural and intellectual. It is harder to learn how to use dependently typed languages and harder to learn how to write a proof of correctness than it is to learn how to write 30 unit tests. Additionally you just need to look at how the industry changes to see that the industry does not trend towards "better" technologies for abstraction. HTML, css, javascript, JAVA, SQL are all awkward/imperfect technologies that dominate the industry for reasons other than technical prowess. Culture dictates their dominance as will it dictate the language of the future. You even get technology that culturally moved backwards simply because people just don't get the importance of static typing... python, php and javascript all came out after typed languages were popular and are all used for large applications where typing would otherwise be very important. Trends like this, and lack of awareness of even algebraic data types tells me that dependent typing is even more unlikely to become popular.
- tsimionescu 7y ago
  > Such programs that are formally correct eliminates the need for testing almost completely and can cut such infrastructure down by possibly 95% I think this is an absurdly high number. The difficulty of proving the kind of rich properties that integration and system-level testing can easily cover is mind-boggling, and also requires huge amounts of infrastructure that doesn't exist and is not feasible for a single team to build. Think of an end-to-end test for a traffic generator application - you simulate a click in a web UI, you start a TCPdump on a network interface, wait for a a few minutes, and sample the capture for some expected packets. How much dependently-typed infrastructure would you need to get even the small level of assurance that this test gives? How much of networking protocols and OS APIs would you have to formally specify to even start proving that your program adheres to them? How much of the DOM and JS APIs would you have to formally specify in order to prove that the button is going to be visible on the screen and that clicking it will produce the right HTTPS calls to the backend? I am reasonably sure that dependent types will continue to get better and will help with developing certain kinds of abstract software components. But I believe that it would take decades before they can become a tool that could be used to prove a realistic large scale program to the point that you can throw away 95% of the testing done today.
cryptica 7y ago
I don't think it's accurate to compare type systems and mathematics. When you write out a mathematical equation, you don't explicitly specify if the variable is a float or an integer or a set or a vector or a matrix as part of the equation, the reader will infer the type of each variable from the problem domain. So in fact, math is much more like dynamically typed languages. >> We know types help us eliminate certain classes of errors from programs. Yes and in my experience they often also introduce new kinds of errors, architectural errors (which are much worse). If you have a system which makes it easier for developers to pass around complex instances across multiple source files, they will use that feature and it will often lead to modules which have lower cohesion and tighter coupling which adds complexity and makes it harder to modify and maintain the logic in the long run. Rigid type systems also add complexity when integrating with third party modules which may use different type names for similar concepts. The wisdom of dynamically typed languages is precisely that it is difficult to know what the type of each variable is so it forces you to follow the logic around (which is unpleasant but necessary). What is almost always overlooked is the human psychological effect; this unpleasantness involved in trying to keep a mental picture of the logic creates a strong incentive for developers to keep the logic as simple, modular/encapsulated as possible. This results in better software design/architecture overall. I'm saying this based on decades of experience having gone back and forth between dynamically and statically typed languages. Programming is as much about human psychology as it is about logic. Dynamically typed languages force developers to be more disciplined and this mindset is extremely valuable. Statically typed languages tend to put developers on auto-pilot. You get so caught up on types and catering to the compiler's warnings that you lose some common sense. Coding in a statically typed language feels a bit like having a boss who micromanages you and tells you every little detail that you need to implement. Coding in a dynamically typed language is more like having a boss which tells you the general picture of what is required and lets you figure out the details. I think the mindset of self-reliance which comes with dynamically typed languages is very important when it comes to producing high quality code.
Koshkin 7y ago
The thing is, the modern notion of what constitutes a type is 'class'. This stealthy switch from one to the other has made the concept of strong typing hard to understand and/or apply in practice, and with the addition of the idea of interfaces, late binding, etc. the problem of types in programming, stated in all its generality, became pretty much intractable.
wellpast 7y ago
I'm forever baffled by the complete inability of our industry to see time or care about seeing that our most precious resource is time. One thing is true: if you're not proving correctness of your code -- formally or informally -- then you are living in entropy and at very high risk of inefficiently delivering value through software. Knowing how to call "correct" on code is paramount. And also -- yes, static type systems allow for (partial) machine verification of these proofs. The missing piece is the innate -- and immense -- cost in having to express these proofs formally in a machine-checkable way. Static type enthusiasts typically downplay these costs but they are simply wrong. I am not talking about the cost of learning how to code in a statically typed system--that should never be factored in. I am talking about the innate costs of formal verification (and strong static typing) that even the expert static typers pay. I have seen these guys work and they are delivering sub-optimally in time compared to the alternatives. Period. I have been around the block with both static and dynamic typing systems and the latter by far optimizes for delivery throughput over time. Formally proving correctness of your program has the upfront cost of formalizing the proof (to the degree required by the verification system) as well has having the effect of crystallizing your code in its current representation which makes it more difficult to (re-)factor for future uses. Some of the (more reasonable) strong static type enthusiasts will concede that this kind of machine/type-proving is better done when the domain and code stabilizes. My hats off to these people for at least being honest about things. However the next realization is that once code and domain stabilize the need/value for machine proving correctness (in typical business/data applications) drops substantially (for obvious reasons). So the pragmatic value of strong type systems and formal verification is far lower than the proponents will have you believe. Of course we've known this truth forever but our industry forgets pretty quickly. Haskell and variants are on the rise in popularity; but make no mistake, if you are optimizing for overall delivery throughput over time -- even experts are swimming upstream with these languages. Of course every time I point this out on HN I get downvoted -- but it kills me to think that a next generation of programmers are being misled down a path of formal purity with misrepresentative claims about the cost of using these tools in real business applications. Just to dispel any idea that what I'm saying is philistinic, I am a mathematician/academic first, enjoy category theory, have written more than my share of academic proofs (including novel results), and think these tools are immensely fascinating. But having been in industry now for 20+ years shipping web-scale and distributed data systems for business industries (what 90+% of us are doing, I imagine), where time is the most precious resource, I know with certainty that leaning on formal verification techniques (including strong static type systems) is an enormous tax compared to the alternative. That these tools work against fast-paced, iterative development. It has also become evident to me that there is a vanguard of static type enthusiast who are not admitting (or perhaps do not understand) the relative cost of the pursuit. Who will point to a few null pointer errors (that, mind you, could be eliminated or reduced by other defensive coding techniques besides formal proofs) and use these to justify the herculean cost of their formal system. If you're a junior or on the fence about static type systems - at least code in a weakly typed PL in which you can lean in one way or the other. If business outcome/throughput is what you value first and foremost, I guarantee you will gravitate more and more toward dynamic evaluation - especially as you realize the world of real business delivery produces constantly changing requirements and carrying out delivery in the face of purist formal modeling and proofs will be a substantial drag on what you can do for little relative benefit downtream.
deleted 7y ago
[deleted]
fny 7y ago
Isn't there a Turing reduction that violates any guarantees? def square(x): maybe_terminate() x*x
mbrock 7y ago
It is quite strange how people assume and spread the notion that types are the best or the only place to put propositions. Why ignore the option of specifying propositions as separate invariants or postconditions, verified by proof, model checking, or testing? Why this focus on Curry-Howard, dependent types, and type theory?
- zozbot234 7y ago
  > Why ignore the option of specifying propositions as separate invariants or postconditions These are usually called 'contracts'. But there's not much of a distinction between contracts and refinement-types.
- tome 7y ago
  I guess it's because the idea of verifying your software in a language that's completely different from the language that you wrote it in seems uncomfortable. If your language is so good, oughtn't it be suitable for expressing its own properties?
ngcc_hk 7y ago
Still think that dynamic language with dynamic type and messaging still have a future. Objective c, lisp and JavaScript have some of this. Not all will die out.
- zozbot234 7y ago
  "Dynamic types" is a misnomer; these are runtime tags in a system of "tagged" values endowed with a single static type. Types apply statically to program expressions, not runtime values. "Messaging" similarly represents the input to a dispatch step-- usually one that introduces non-trivial pitfalls if you want to ensure that your code keeps making sense as it evolves (see "fragile base class" and the like). Anyway, dependently-typed languages support these patterns better than most other static languages do, since static types can trivially be reified as runtime-tagged data in such languages, while keeping the ordinary benefits of static typing for most of the code.

74 points by lewisjoe 7y ago

azhenley 7y ago

Anyone know who wrote this?

fauigerzigerk 7y ago
I don't know, but I wouldn't be surprised if he did: https://github.com/joelewis https://github.com/joelewis

karmakaze 7y ago

What's the purpose of posting as a G-Doc instead of HTML? The visitors' google account info could potentially be collected.

3pt14159 7y ago
Not really anymore. It's now anonymized by default.
- nixpulvis 7y ago
  Color me skeptical. Plus it breaks the "visited" styling on HN, and generally pisses me off for throwing me out of my browser. <angry old man waves fist at cloud />
BLanen 7y ago
Or just a pdf uploaded to wherever. Even google Drive.

malkia 7y ago

The webpage for AGDA seems to be https://github.com/agda/agda https://github.com/agda/agda or https://wiki.portal.chalmers.se/agda/pmwiki.php https://wiki.portal.chalmers.se/agda/pmwiki.php, but not https://www.agda.com.au/ https://www.agda.com.au/ (end of the paper).

lewisjoe 7y ago
Thanks. Fixed the links.

lidHanteyk 7y ago

I'd like to joke that we could replace the link with [0] and it would be a massive improvement. Seriously, though, these descriptions of type-theoretic programming as a solution to a problem, rather than a tower to be climbed, are increasingly obscurantist, hiding the meat of the correspondence behind analogies and narratives. [0] https://ncatlab.org/nlab/show/computational+trinitarianism https://ncatlab.org/nlab/show/computational+trinitarianism

carapace 7y ago
> hiding the meat of the correspondence behind analogies and narratives. Interesting. Could you elaborate a little?
- lidHanteyk 7y ago
  Sure. Any time somebody says "Curry-Howard" and doesn't provide the table that I provided, they are handwaving. The table makes the correspondence precise.
  - carapace 7y ago
    Cheers. When you say "the correspondence behind analogies and narratives", which column is analogy and which is narrative? I hope I'm not being really dense or ignorant here, apologies if so.
    - lidHanteyk 7y ago
      The page I linked is relatively clear. I was complaining about the original article, which fails to make contact with the actual guts of formal type theory.
      - carapace 7y ago
        Right, I get that. But the words "analogy" and "narrative" don't appear in the page. I'm wondering what you mean by those words?

abeppu 7y ago

This author predicts that we'll drift towards languages like Agda or Idris, and also discusses how type systems came out of math. I'm curious about two related questions: 1. Why is it that a minority of math is done with proof systems (i.e. yielding automatically checkable artifacts)? It's burdensome to formalize much of the math that we're interested, even when we're confident in that math. What's the nature of that burden, and how could tools improve to lessen it? 2. Are the difficulties which prevent a lot of math from being done with these systems the same as the difficulties which prevent programmers from using them? There are many invariants that we can easily know about a program, but representing the lot of them in types would be onerous. How do we make that easier/lighter?

zozbot234 7y ago
> Why is it that a minority of math is done with proof systems (i.e. yielding automatically checkable artifacts)? Because most interesting math depends on a lot of other math, and formalizing all of these pre-requirements is a significant burden. The math subfields where this is less of a problem (so-called 'synthetic' mathematics) are also where formalization is being used the most.
- Smaug123 7y ago
  And additionally it takes a lot of effort to formalise a proof. (I say this as someone who has spent nearly two years formalising basic maths in Agda.) It's true in maths as in programming: 90% of the work is in the last 10%, and if you don't get the last 10%, you haven't got a proof.
  - zozbot234 7y ago
    The usual rule of thumb is that 1 page of paper proof leads to 4 pages of "proper" formal proof. Though this may vary depending on how capable the proof assistant is - AIUI, Agda requires you to write out complete proof terms, whereas other systems may be more capable. Sometimes you can use a kind of "reflection" that makes many proofs trivial, simply by defining a decision procedure that's proven to be correct in the general case, and having the system perform the appropriate computations. This is how you would deal, e.g. with trivial simplifications in elementary algebra (that can usually be proven to be valid in any ring, field etc.)

pcwalton 7y ago

We aren't going to move to dependently-typed languages based around theorem proving anytime soon. The reason is simple: those languages don't support normal industry development practices, where you don't have time to spend 10x the time on verification as you do on development. (They do support development practices favored by the US Department of Defense, which is perhaps part of the reason why research into such type systems attracts DARPA grants.) Where such languages may have a future is for proving some kernel of core infrastructure code correct, where the code has such a high value to size ratio that spending the time to prove it correct may cross the line into economic viability. SeL4 is a high-profile example of this. Another example that's been on my mind over the years could be proving the unsafe code in the Rust standard library correct. The latter would be interesting because it would address the criticism of "well, there's unsafe code in libstd, how can you say Rust is safe?" without burdening regular Rust users (not standard library developers) with all the baggage of a complex type system.

zozbot234 7y ago
> The reason is simple: those languages don't support normal industry development practices, where you don't have time to spend 10x the time on verification as you do on development. In practice, these languages have good support for gradual development so no, you don't have to spend 10x your dev time on verification. You can focus your verification effort on the lowest-hanging fruit, such as properties that only depend on local reasoning, as opposed to non-trivial interactions involving the program as a whole. (One potential issue for this is that dependently-typed languages are total languages, so any code that's 'natively' written in the languages must be proven to terminate. But partiality and Turing-completeness can be reintroduced in a fairly trivial way by resorting to a 'Delay' or 'Partial' monad.)
phillipcarter 7y ago
There’s also the problem where inferring the types is not decidable, so we either get slow tooling/builds or an onerous development cycle of specifying everything. The latter would be unbearable when you consider how weird and annoying things relate to one another in large, enterprisey systems.

smitty1e 7y ago

What I'd like to locate/implement would be: - an in-memory SQLite database with - a sufficiently generalized schema that could - ingest the static type information emitted by, say GCC, so that - one could easily inspect/compare metadata from any language. I doubt that this idea is unique to me.

Boulth 7y ago
Sounds like Language Server: https://langserver.org/ https://langserver.org/
- smitty1e 7y ago
  Same idea carried further to include data types and objects that actual programs in the languages use, not just the EBNF grammar constructs of the languages. Unless I missed that in my quick glance at the link.
  - Boulth 7y ago
    Yep, LSP does include semantic view of the code. That is anything you'd see at the end tools such as IDEs: types, members, functions, properties within context (e.g. this function is a member of this class).
oscargrouch 7y ago
If im not mistaken, what you want is basically this: https://kythe.io/ https://kythe.io/ Also lets not forget that LLDB can basically be that (at least for LLVM languages) https://lldb.llvm.org/resources/architecture.html https://lldb.llvm.org/resources/architecture.html "LLDB converts debug information into Clang types so that it can leverage the Clang compiler infrastructure. This allows LLDB to support the latest C, C++, Objective-C and Objective-C++ language features and runtimes in expressions without having to reimplement any of this functionality." By the way, Visual Studio and Code with the C++ plugin is using the embedded version of SQL Server database.. so they probably have this sort of architecture, for index, debugging, etc.. So somewhere they might at least decribe how they (Microsoft) are doing this in Visual Studio architecture.

crimsonalucard 7y ago

LEAN is another popular language in this area. There are huge benefits for moving the industry in this direction. Such programs that are formally correct eliminates the need for testing almost completely and can cut such infrastructure down by possibly 95%. A program can use dependent typing to prove itself 100% correct vs. 100 unit tests which proves only 100 arbitrary test cases as correct. Unit tests are statistical experiments where the people hope that the verification of 100 arbitrary test cases correlates with the entire program being correct. Yes, proofs are harder to write than tests, yes there can be bugs in your proof (their can be bugs in tests too). However, I genuinely believe that for the lifetime of an application, in general, the net benefits of dependent types is positive and greater than that provided by testing. However I do not believe the industry will move in this direction. The reason why the industry won't move in this direction is largely cultural and intellectual. It is harder to learn how to use dependently typed languages and harder to learn how to write a proof of correctness than it is to learn how to write 30 unit tests. Additionally you just need to look at how the industry changes to see that the industry does not trend towards "better" technologies for abstraction. HTML, css, javascript, JAVA, SQL are all awkward/imperfect technologies that dominate the industry for reasons other than technical prowess. Culture dictates their dominance as will it dictate the language of the future. You even get technology that culturally moved backwards simply because people just don't get the importance of static typing... python, php and javascript all came out after typed languages were popular and are all used for large applications where typing would otherwise be very important. Trends like this, and lack of awareness of even algebraic data types tells me that dependent typing is even more unlikely to become popular.

tsimionescu 7y ago
> Such programs that are formally correct eliminates the need for testing almost completely and can cut such infrastructure down by possibly 95% I think this is an absurdly high number. The difficulty of proving the kind of rich properties that integration and system-level testing can easily cover is mind-boggling, and also requires huge amounts of infrastructure that doesn't exist and is not feasible for a single team to build. Think of an end-to-end test for a traffic generator application - you simulate a click in a web UI, you start a TCPdump on a network interface, wait for a a few minutes, and sample the capture for some expected packets. How much dependently-typed infrastructure would you need to get even the small level of assurance that this test gives? How much of networking protocols and OS APIs would you have to formally specify to even start proving that your program adheres to them? How much of the DOM and JS APIs would you have to formally specify in order to prove that the button is going to be visible on the screen and that clicking it will produce the right HTTPS calls to the backend? I am reasonably sure that dependent types will continue to get better and will help with developing certain kinds of abstract software components. But I believe that it would take decades before they can become a tool that could be used to prove a realistic large scale program to the point that you can throw away 95% of the testing done today.

cryptica 7y ago

I don't think it's accurate to compare type systems and mathematics. When you write out a mathematical equation, you don't explicitly specify if the variable is a float or an integer or a set or a vector or a matrix as part of the equation, the reader will infer the type of each variable from the problem domain. So in fact, math is much more like dynamically typed languages. >> We know types help us eliminate certain classes of errors from programs. Yes and in my experience they often also introduce new kinds of errors, architectural errors (which are much worse). If you have a system which makes it easier for developers to pass around complex instances across multiple source files, they will use that feature and it will often lead to modules which have lower cohesion and tighter coupling which adds complexity and makes it harder to modify and maintain the logic in the long run. Rigid type systems also add complexity when integrating with third party modules which may use different type names for similar concepts. The wisdom of dynamically typed languages is precisely that it is difficult to know what the type of each variable is so it forces you to follow the logic around (which is unpleasant but necessary). What is almost always overlooked is the human psychological effect; this unpleasantness involved in trying to keep a mental picture of the logic creates a strong incentive for developers to keep the logic as simple, modular/encapsulated as possible. This results in better software design/architecture overall. I'm saying this based on decades of experience having gone back and forth between dynamically and statically typed languages. Programming is as much about human psychology as it is about logic. Dynamically typed languages force developers to be more disciplined and this mindset is extremely valuable. Statically typed languages tend to put developers on auto-pilot. You get so caught up on types and catering to the compiler's warnings that you lose some common sense. Coding in a statically typed language feels a bit like having a boss who micromanages you and tells you every little detail that you need to implement. Coding in a dynamically typed language is more like having a boss which tells you the general picture of what is required and lets you figure out the details. I think the mindset of self-reliance which comes with dynamically typed languages is very important when it comes to producing high quality code.

Koshkin 7y ago

The thing is, the modern notion of what constitutes a type is 'class'. This stealthy switch from one to the other has made the concept of strong typing hard to understand and/or apply in practice, and with the addition of the idea of interfaces, late binding, etc. the problem of types in programming, stated in all its generality, became pretty much intractable.

wellpast 7y ago

I'm forever baffled by the complete inability of our industry to see time or care about seeing that our most precious resource is time. One thing is true: if you're not proving correctness of your code -- formally or informally -- then you are living in entropy and at very high risk of inefficiently delivering value through software. Knowing how to call "correct" on code is paramount. And also -- yes, static type systems allow for (partial) machine verification of these proofs. The missing piece is the innate -- and immense -- cost in having to express these proofs formally in a machine-checkable way. Static type enthusiasts typically downplay these costs but they are simply wrong. I am not talking about the cost of learning how to code in a statically typed system--that should never be factored in. I am talking about the innate costs of formal verification (and strong static typing) that even the expert static typers pay. I have seen these guys work and they are delivering sub-optimally in time compared to the alternatives. Period. I have been around the block with both static and dynamic typing systems and the latter by far optimizes for delivery throughput over time. Formally proving correctness of your program has the upfront cost of formalizing the proof (to the degree required by the verification system) as well has having the effect of crystallizing your code in its current representation which makes it more difficult to (re-)factor for future uses. Some of the (more reasonable) strong static type enthusiasts will concede that this kind of machine/type-proving is better done when the domain and code stabilizes. My hats off to these people for at least being honest about things. However the next realization is that once code and domain stabilize the need/value for machine proving correctness (in typical business/data applications) drops substantially (for obvious reasons). So the pragmatic value of strong type systems and formal verification is far lower than the proponents will have you believe. Of course we've known this truth forever but our industry forgets pretty quickly. Haskell and variants are on the rise in popularity; but make no mistake, if you are optimizing for overall delivery throughput over time -- even experts are swimming upstream with these languages. Of course every time I point this out on HN I get downvoted -- but it kills me to think that a next generation of programmers are being misled down a path of formal purity with misrepresentative claims about the cost of using these tools in real business applications. Just to dispel any idea that what I'm saying is philistinic, I am a mathematician/academic first, enjoy category theory, have written more than my share of academic proofs (including novel results), and think these tools are immensely fascinating. But having been in industry now for 20+ years shipping web-scale and distributed data systems for business industries (what 90+% of us are doing, I imagine), where time is the most precious resource, I know with certainty that leaning on formal verification techniques (including strong static type systems) is an enormous tax compared to the alternative. That these tools work against fast-paced, iterative development. It has also become evident to me that there is a vanguard of static type enthusiast who are not admitting (or perhaps do not understand) the relative cost of the pursuit. Who will point to a few null pointer errors (that, mind you, could be eliminated or reduced by other defensive coding techniques besides formal proofs) and use these to justify the herculean cost of their formal system. If you're a junior or on the fence about static type systems - at least code in a weakly typed PL in which you can lean in one way or the other. If business outcome/throughput is what you value first and foremost, I guarantee you will gravitate more and more toward dynamic evaluation - especially as you realize the world of real business delivery produces constantly changing requirements and carrying out delivery in the face of purist formal modeling and proofs will be a substantial drag on what you can do for little relative benefit downtream.

deleted 7y ago

[deleted]

fny 7y ago

Isn't there a Turing reduction that violates any guarantees? def square(x): maybe_terminate() x*x

mbrock 7y ago

It is quite strange how people assume and spread the notion that types are the best or the only place to put propositions. Why ignore the option of specifying propositions as separate invariants or postconditions, verified by proof, model checking, or testing? Why this focus on Curry-Howard, dependent types, and type theory?

zozbot234 7y ago
> Why ignore the option of specifying propositions as separate invariants or postconditions These are usually called 'contracts'. But there's not much of a distinction between contracts and refinement-types.
tome 7y ago
I guess it's because the idea of verifying your software in a language that's completely different from the language that you wrote it in seems uncomfortable. If your language is so good, oughtn't it be suitable for expressing its own properties?

ngcc_hk 7y ago

Still think that dynamic language with dynamic type and messaging still have a future. Objective c, lisp and JavaScript have some of this. Not all will die out.

zozbot234 7y ago
"Dynamic types" is a misnomer; these are runtime tags in a system of "tagged" values endowed with a single static type. Types apply statically to program expressions, not runtime values. "Messaging" similarly represents the input to a dispatch step-- usually one that introduces non-trivial pitfalls if you want to ensure that your code keeps making sense as it evolves (see "fragile base class" and the like). Anyway, dependently-typed languages support these patterns better than most other static languages do, since static types can trivially be reified as runtime-tagged data in such languages, while keeping the ordinary benefits of static typing for most of the code.