I've solved production problems with Haskell (including w/advanced type system features & dependent types). I will continue to do so. And I will probably write other commercial, money-making software for enterprises and for myself for years to come.
I have plenty of experience programming in other languages. Clojure, Go, Java, Python. Haskell was the hardest to pick up. But now that I know it, writing other languages requires so much more energy in comparison. I barely have to try to deliver equal results compared to solving the same problems with other tools (so it's not a result of me just increasing my skill - the tool itself is a force multiplier for myself 100%)
What I said was that Haskell's design and evolution have been primarily guided by research questions rather than business needs, not that it's unsuitable for production use. I didn't say it's unsuitable for production use, nor do I think it. That doesn't change the pretty obvious fact that its features are mostly guided by research questions.
> barely have to try to deliver equal results compared to solving the same problems with other tools (so it's not a result of me just increasing my skill - the tool itself is a force multiplier for myself 100%)
If that effect were scalable and largely universal, then there would be no need for this discussion, anyway. But if it works well for you and the other thousands of developers who make up ~0.06% of the market, then it's great that it's available. Research languages also serve a very valuable goal in figuring out what works and what doesn't. If no one used them, we wouldn't know.
99 bottles of beer with state monads gets at some of the challenge for the neophyte:
http://www.99-bottles-of-beer.net/language-haskell-1360.html
Look at the struggle going on to deal with a "simple" piece of state.
On the other hand this blog post http://www.haskellforall.com/2013/05/program-imperatively-us... demonstrates how one of the bits of Haskell that some people find complex (lenses) can be used together with the state monad to provide an "imperative-like" experience that's even nicer than most imperative languages.
For instance, it defines a Beer datatype, yet stores a plain Int in the state, then casts it to Beer only to use a custom pretty printer, instead of creating a verse :: Int -> String, or verse :: Beer -> String function.
Out of interest, what kind of software do you build with Haskell? I'm doing web stuff and haven't quite been able to decide whether to stick to Haskell or Elixir for my own projects.
In my free time I'm making games in Haskell, but that's slow-going partially due to the ecosystem not being mature but mostly due to lack of free time :)
That doesn't particularly bother me in Haskell, which was born as, and continues to primarily serve as, a platform for language research. (Secondary purpose, at least for me: A platform for daydreaming about a non-post-C++ existence. I suspect that professional use remains a small minority.) It gets more worrisome to me in an ostensibly industry-oriented language like Scala. There I start to fear that my colleagues choose ways of solving problems for about the same reasons that I prefer mechanical watches over quartz ones: Not because they're more practical or more economical - no in both cases - but because they're cooler.
I think it'll probably get better naturally, though, the same way that lisp programming culture eventually stopped being quite so enamored of macros, and Java programming culture eventually stopped being quite so enamored of elaborate XML configuration files.
Python programmers say the same about all static type systems. What alternatives do you have in mind? Are they as generally applicable as dependant types? Dependant types are a simple and unifying way to solve a variety of shortcomings with conventional statically typed systems. For example, dependant types can express first-class modules as simple records, or allow sophisticated record operations like merge to be well-typed.
> [tracking algebraic effects] But is that even a worthwhile goal? Why is it nirvana to more easily do something that might not be worth doing at all?
Given the various hugely expensive bugs I have been involved in (e.g. Java toString on a date reading the system locale). I would say yes. In my industry, reproducable numbers are of vital importance, so much so that the quants use Haskell in preference to something more mainstream and supported.
So what? Even if you think having X is good, that doesn't mean having 100X is necessarily better.
> Dependant types are a simple and unifying way to solve a variety of shortcomings with conventional statically typed systems.
But solving problems with type systems is not a business goal. Increasing correctness is.
> What alternatives do you have in mind?
The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods. Dependent types are a powerful, general and complex mechanism that only scales well for very simple problems.
> Given the various hugely expensive bugs I have been involved in (e.g. Java toString on a date reading the system locale). I would say yes.
There are easier ways, like Java's permission system, that I mentioned elsewhere.
Model checking is great, and many tools developed by the model checking community are marvellous (especially the TLA+ model checker).
But deductive methods scale well enough to definitively establish integrity and confidentiality for an entire OS kernel. They scale well enough to show that that said kernel has no in-kernel storage channels that can be exploited in a side channel attack.
Deductive methods scale well enough to verify (completely automaticallly, without human intervention) that the compiled binaries faithfully implement a given C program, so the compiler and linker need not be trusted.
These are deep properties. You're welcome to give examples of model checking or concolic testing establishing comparably deep properties of actual code of comparable length (not algorithm sketches or high-level system descriptions, actual code that compiles and runs).
That's for deductive approaches in general. But sone of your specific claims about type theory are dubious as well. Elsewhere you claim that
> The fact that even current formal verification research is mostly looking elsewhere seems to suggest that the answer is likely negative
Your claim that formal methods research is mostly looking elsewhere is really stretching it. More researchers are doing type theory than ever. Grants are pouring in, some labs can offer 20+ PhD scholarships per year. The number of submissions to ICFP's TyDe track had over 30% growth last year. TYPES already dwarfs the biggest conferences devoted to model checking or any other specific formal method. No widely cited research aeticles express the sentiment that "type theory has failed and we should look elsewhere". No other subfields are ezperiencing comparable growth.
Unfortunately, they do not. The two projects you mentioned are positively tiny -- they correspond to about 10KLOC of C, or less than 1/5th the size of jQuery -- and they each took world experts years of effort. Both, BTW, required serious limitations in the algorithms used to keep them simple. That's like saying that transmuting lead into gold scales well because we can transmute ten gold atoms in a billion-dollar particle accelerator.
> You're welcome to give examples of model checking or concolic testing establishing comparably deep properties of actual code of comparable length
Concolic tests are unsound, which is why they scale so well. Model checking routinely verifies much larger codebases, so much so that people don't bothering writing papers about it. When deductive methods are used to verify a 10KLOC program that's news. You can buy off-the-shelf model checkers that do more in industry pretty much all the time.
> More researchers are doing type theory than ever. Grants are pouring in, some labs can offer 20+ PhD scholarships per year.
Perhaps, but when you look at FM conferences, deductive methods in general and type systems in particular are significantly more represented.
> No widely cited research aeticles express the sentiment that "type theory has failed and we should look elsewhere"
There's no need to abandon something that has yet to break through in the first place. Most FM research is just done elsewhere.
> No other subfields are ezperiencing comparable growth.
Automated methods are.
When you establish actual deep properties, that's news. You can't buy any model checker that verifies confidentiality for actual kernels. At all. There is no such model checker.
Again, if non-deductive formal methods are routinely used to establish comparably deep properties of programs of comparable size (as you claim), you should have no trouble naming at least one example. You don't need research papers to justify that claim, just a few statements of the form "Global Property P of 10k line C Program Q was established by model checker R".
> That's like saying that transmuting lead into gold scales well because we can transmute ten gold atoms in a billion-dollar particle accelerator.
No, not really. NICTA kept tabs on this, and got that producing seL4 costs about 50% more per line of code than other commercial L4 microkernels. While that is a significant expense, there is no order of magnitude difference, much less something in the "billion dollar particle accelerator" territory. Especially since it delivered global correctness properties that are out of reach for any other method.
Model checkers don't usually beat deductive proofs in both size and depth, but they often easily beat them on any one of these.
In terms of code size, model checkers have verified reachability on C programs of over 50KLOC in less than an hour for at least 15 years now (BLAST). Some bugs found in the past few years Linux kernel with a model checker are here: http://linuxtesting.org/results/ldv-cpachecker
In terms of depth -- there are too many to choose from. Both SCADE and Simulink are routinely used in industry to verify LTL. TLC, a model checker for TLA+ was used to develop and verify deep properties of the OpenComRTOS kernel https://en.wikipedia.org/wiki/OpenComRTOS
> You can't buy any model checker that verifies confidentiality for actual kernels. At all. There is no such model checker.
There is no real method like this of any kind. A heroic effort by teams of PhD candidate proof monkeys working for some years isn't a technique.
> not really. NICTA kept tabs on this, and got that producing seL4 costs about 50% more per line of code than other commercial L4 microkernels.
I don't know what the cost of producing commercial L4 microkernels, but that 10KLOC program took 12 person years, plus another 12 for tooling. 2 years per KLOC, and even half of that, is well beyond the reach of 99% of software, plus no one has ever managed to use deductive verification for programs that are significantly larger than that in any amount of time. That's about three (!) orders of magnitude behind ordinary business software. This gap has remained pretty much constant over the last forty years.
I think it is possible that deductive proofs may become viable in industry in some high-assurance, high-cost domains, provided that the programs are very small. But there is no sign that it could reasonably be a basis for increasing correctness of more ordinary software.
Deductive methods the assembly refinement proof of seL4 (binary verification) is completely automated, and takes less than two hours on a modern PC.
OpenComRTOS is much much smaller and simpler than seL4 (comparable to eChronos). It's important work, and a neat example at how formal modeling allows one to _design better products_ even in well-explored domains, but it's a really poor example for illustrating the supposed scalability of model checking compared to deductive methods. Especially ehen the book on the system emphasizes how they kept experiencing state explosions which broke the checker during development.
In any case, TLC checks specifications, not implementations; it's not appropriate to compare them to deductive methods that work on actual source code (cf. the properties of the _specification_ account for less than 5% of total proof obligations, and establish global properties that are stronger and deeper than model checking could provide). Attempts to use TLA+ on implementations such as C2TLA+ are far less successful, it's not been demonstrated to scale well (no case studies above 1 kloc at all). Writing and checking specifications is useful, and leads to more reliable software, and you're free to argue that there is far more low-hanging fruit to be found in this area than in dependent type systems. But it's not the same as checking 50kloc _programs_, and you should not conflate these activiities.
Not to say that many deductive tools are completely automated and have been shown to work at scale too: SydTV verifies the correspondence between thr seL4 binary and the corresponding sourcr in under two hours on a modern PC.
And what you're competing against (dependent types) has the potential to scale far better: even the 3.5kloc Agda program I'm working on can be checked in under a minute, and Agda is very far from optimal with respect to type checking.
> But there is no sign that it could reasonably be a basis for increasing correctness of more ordinary software.
You're entitled to that opinion. Just don't conflate that with general trends and sentiments in the formal methods community. Contrary to your earlier claims, there is no agreement in the field that one should "look elsewhere".
The same goes for your claim that non-deductive techniques scale better and establish deeper properties than deductive ones: if you believe this will be shown decisively true in the future, that's a perfectly alright opinion to have, and you'll find plenty of peiple who share it. But don't act as if it's an empirical fact when the evidence shows no such scalability advantage at this point in time, and most deep properties that deductive, proof-producing methods can establish are still out of reach for non-deductive methods.
(ps. Writing these posts took me a lot of time, so I'll have to limit myself to one more comment in this thread.)
TLC checks specifications of arbitrary detail. I don't see why it matters when it comes to deep properties. There does not exist any method -- automated or manual -- that can verify deep properties of code of size even within an order of magnitude of ordinary applications. Inasmuch as model checkers and deductive proofs work at all, model checkers are clearly more scalable.
> But it's not the same as checking 50kloc _programs_, and you should not conflate these activities.
I explicitly said that model checkers don't beat deductive proofs on size and depth at the same time, but they do beat them easily separately. Still, there are a few cases where model checkers fail, and the only option available is formal proof. Usually, that is too expensive, but we have seen that in extreme circumstances when a great amount of work is applied to a very small amount of code, this could "work" in the sense that specialized, highly-trained teams working for a long time could do it. AFAIK, this has so far only been tried in research projects, and never by "ordinary" engineers.
> And what you're competing against (dependent types) has the potential to scale far better: even the 3.5kloc Agda program I'm working on can be checked in under a minute, and Agda is very far from optimal with respect to type checking.
If checking a proof were comparable to finding one, then the P vs NP problem would have been resolved a long time ago. You should compare the time it takes to write and model-check a 3500-line TLA+ spec vs the time it takes to write a 3500 line Agda program and check the proofs.
> Contrary to your earlier claims, there is no agreement in the field that one should "look elsewhere".
I didn't say there was consensus; I said that the majority of researchers are looking elsewhere, and that's where most research is focused.
> But don't act as if it's an empirical fact when the evidence shows no such scalability advantage at this point in time, and most deep properties that deductive, proof-producing methods can establish are still out of reach for non-deductive methods.
Deductive methods have been studied for at least forty years now, and AFAIK, they have never been used in any meaningful scale by non-researchers in industry. On the other hand, while automated methods obviously have not reached the point that they could automatically verify arbitrary properties of arbitrarily sized code -- and they never will, and neither will deductive methods -- they are being used in industry on a regular basis, with capabilities ranging on depth, scale, and soundness, and their use is growing; just in the safety-critical space where SCADE and Simulink are used, but at Microsoft, Amazon, Oracle and Facebook as well as smaller companies. As an applicable formal method in the real world, deductive proofs don't even exist yet, heroic efforts by researchers notwithstanding.
Which is why it's unsurprising that more researchers are looking into methods that have had some measure of success outside research. I find all aspects of formal methods very interesting, and I wish all researchers luck and success (and I sometimes amuse myself with small machine-checked proofs, usually in the TLA+ proof assistant or sometimes in Lean), but it is misleading to present deductive and automated methods as being on equal footings in terms of real-world success.
I also think there is a fundamental mismatch between deductive proofs and software verification, something I call the "soundness problem." Unlike mathematics, while an algorithm can be proven correct, a software system never can, any more than a chair could -- it's a physical system. This means that soundness is never, ever, ever a requirement in software verification. On the other hand, achieving soundness (for deep properties) is very costly, as both theory and experience tell us. This is why many experiments these days -- both in academia and industry -- try to turn down the soundness knob to achieve other actual requirements in software verification (see O'Hearn's recent "incorrectness logic"). A method that is inflexible on soundness -- which is both not required and very costly, is one that seems to be clashing with the very needs of software verification.
This is also why you find that research projects using deductive proofs are almost invariably done by people with little or no industry experience. They treat the problem of software verification as an academic exercise without understanding what real software is and how it's used. On the other hand, you see many more researchers with industry experience looking into automated methods. It's funny, to see the transformation. You look at someone like Peter O'Hearn that's moved from academia to industry. What does he do then? Turn down soundness. You also see it with Leslie Lamport and David Harel, and I could probably find more examples. Once researchers are faced with how software is actually developed, the first thing they realize you need to do is to reduce soundness (for deep properties). Soundness is not a requirement, and it is the enemy of scale and speed, which are (I've written a short post on one aspect where researchers don't understand how software is written: https://pron.github.io/posts/people-dont-write-programs). There are cases in software where soundness is needed -- automatic refactoring and compiler optimization -- which is why I think type systems are interesting for those, but correctness -- not so much.
On the other hands approaches to correctness based on dependent types are favored by people who may be very good researchers, but are not professional programmers, not familiar with industry, and have not conducted field studies (people like Bob Harper, Adam Chlipala, Edwin Brady, and Leonardo de Moura). Now, their research is very good, but it is theoretical, and so far unsuitable for any field use, which is unsurprising, given that they're unfamiliar with how software is made. Which brings me back to my original point: bringing dependent types to Haskell is an interesting first field experiment, but it is just that -- a research experiment designed to answer a research question (someone who worked on seL4 told me that they believe they could bring the cost down enough to be similar to that of high-assurance software, but that's not where Haskell is or, I think, wants to be). It is very different from the kind of work that people like O'Hearn and Lamport are doing, which is scaling up approaches that have already shown their worth in the field.
better scalability than
deductive
- Scalable to large code bases.
- Scalable to deep properties.
Deductive methods are currently the only ones that scale to deep properties. Model checking et al are currently the much better at scaling to large code bases. Note however two things: First, Facebook's infer tool which scales quite well to large code bases, is partly based on deductive methods. Secondly, and most importantly, under the hood in most current approaches, SAT/SMT solvers do much of the heavy lifting. Existing SAT/SMT solvers are invariably based on DPLL, i.e. resolution, i.e. a deductive method.
Model checkers check deep properties with overall significantly less effort. It is true that they don't always succeed, but neither do deductive proofs. In industry, deductive methods are used as a last resort, when they're used at all, to tie together results from automated techniques.
> Note however two things: ...
That's not what I meant by "deductive methods;" I meant verification by semi-automated deductive proofs. Also, SMT solvers aren't used in isolation to verify significant pieces of software, they're used as components of model checkers, concolic testing and proof assistants (or to verify local properties of code units), so they're used in both semi-automated deductive methods as well as in automated methods. I also believe that DPLL is based on assignment and backtracking, not resolution.
Model checkers check deep
DPLL is based
TLC is a model checker can check most properties expressible in TLA+, which are more expressive than any base lambda-calculus theory (e.g. it includes temporal refinement properties). See my overview on TLA+'s theory: https://pron.github.io/tlaplus
> in real implementations you mostly simply enumerate models, and backtrack (maybe with some learning) if you decided to abandon a specific model
So not deductive. You know that because DPLL does not directly yield a proof of UNSAT.
can check most properties
expressible in TLA+
- Assume we 'measure' the complexity of a property by the number of quantifier alternations in the logical formula.
- Assume we 'measure' the complexity of a program by lines of code.
(Yes, both measures are simplistic.) What is the most complex property that has been established in TLA fully automatically with no hand tweaking etc for more than 50,000 LoCs? And how does that complexity compare to for example the complexity of the formula that has been used in the verification of SeL4?
So not deductive.
There is an interesting question here: what is the precise meaning of "deductive"? Informally it means: building proof trees by instantiating axiom and rule scheme. But that is vague. What does that mean exactly? Are modern SAT/SMT solvers doing this? The field of proof complexity thinks of (propositional) proof systems simply as poly-time functions onto propositional tautologies.
TLC, a model checker for TLA+, is commonly used to verify arbitrary properties -- at least as "deep" as those used in seL4, and often deeper -- of TLA+ specifications of a few thousand lines. Those properties can informally correspond to codebases with hundreds of thousands of lines, but there is currently no method for formally verifying arbitrary properties of 50KLOC, be it automatic or manual. Automated methods, however, are used either for deep properties (quantifier alterations) of few k-lines of spec/code or shallower (though still non-local and non-compositional) properties of 50-100KLOC. Manual deductive methods are virtually used for nothing outside of research projects/teams, except for local, compositional properties, of the kind expressible by simple type systems.
I clarified further here: https://news.ycombinator.com/item?id=22146186
> So first-order logic is not deductive, because it doesn't yield a direct proof of FALSE?
In any logic you can work deductively in the proof theory, or in the model theory. DPLL SAT solvers work in the model theory of first-order logic. Also, SAT solvers work on propositional logic, not first-order logic. Because of completeness, we know that every model-theoretic proof corresponds to a proof-theoretic proof, but that's not how most SAT algorithms work (except for resolution solvers).
> There is an interesting question here: what is the precise meaning of "deductive"?
It means using the syntactic inference rules of a proof theory, rather than the semantic rules of a model theory (possibly relying on completeness meta-theorems, as in the case of propositional logic, although that's not relevant for most interesting first-order theories). SMT solvers employ SAT, and can work on some first-order theories. I am not familiar with all the techniques SMT solvers use, but I believe they employ both proof-theoretic and model-theoretic techniques. In any event, as I mentioned before, SMT solvers are rarely used alone, because they're very limited. They are used as automated helpers for specific steps in proof assistants (TLAPS, the TLA+ proof assistant makes heavy use of SMT solvers for proof steps), for local properties of code (e.g. OpenJML for Java, in Dafny and in SPARK) or as components in CEGAR model checkers and in concolic test systems.
TLC ... is commonly used to ...
at least as "deep" as those
used in seL4, and often deeper
One problem with model-checking is that you handle loops by replacing loops with approximations (unrolling the loop a few times) and in effect only verifying properties that are not affected by such approximations. In other words extremely shallow properties. (You may use different words, like "timeout" or "unsound technique" but from a logical POV, it's all the same ...)
the model theory ...
rather than the semantic
rules of a model theory
With that, what mathematicians call a model is but another deductive theory, e.g. the model theory of Peano Arithmetic happens in ZFC, another deductive theory. The deductive/non-deductive distinction is really a discussion of different kinds of algorithms. Deduction somehow involves building up proof trees from axioms and rules, using unification. It could be fair to say that concrete DPLL implementations (as opposed to textbook presentations) that are based on model enumeration, non-chronological backtracking, random restarts, clause learning, watched literals etc don't quite fit this algorithmic pattern. I am not sure exactly how to delineate deductive from non-deductive algorithms, that's why I think it's an interesting question.
SMT solvers are rarely used alone,
* * *
No, I am not. Read what I wrote again :)
> and please don't forget to collect your Turing Award!
Some people have already beat me to it. The 2007 Turing Award was awarded for the invention of model checkers that precisely and soundly check deep properties.
> One problem with model-checking is that you handle loops by replacing loops with approximations
No, that's what sound static analysis with abstract interpretation does. Model checkers are both sound and precise, i.e. they have neither false positives nor false negatives. To the extent they use sound abstraction (i.e. over-approximation), as in CEGAR algorithms, they do so to increase performance and to sometimes be able to handle infinite state spaces. A model checker, however, is always sound and precise, or else it's not a model checker.
> In other words extremely shallow properties.
Model checkers commonly check arbitrarily deep properties. Engineers in industry use them for this purpose every day.
> All mathematics is deductive.
Yes, and all (or much, depending on your favorite philosophy of mathematics) of it has models. If you have two apples in one hand and one apple in the other and you count how many you have, you have not done so using deduction in any logical theory. That had you used such a process you would have also reached the same result is because of soundness and completeness meta-theorems. That mathematics has both proof and model theories, and that they're compatible, is the most important result in formal logic.
> All I'm saying is that they too have scalability limits, just that the scale involved here is not lines of code.
All verification methods are limited by both size of code and depth of properties. For non-trivial property, the least scalable method, on average, is deductive proof. Which is not to say it is not useful when automated methods have failed.
Be that as it may, seL4 cannot currently be automatically verified, and it's not due to code size (8700 lines of C and 600 lines of assembler). It's hard to see what the obstacle to mechanisation could be but logical complexity.
Model theory is not some magical deduction-free paradise. The reason we care about model theory in logic is because we want to have evidence that the deductive system at hand is consistent. Building models of Peano arithmetic in ZFC for example, but also relating constructive and classical logic through double negation or embedding type theory in set theory, are all about relative consistency. It's easy to make a FOM (= foundation of mathematics) unsound, and logical luminaries including Frege, Church and Martin-Lof managed to do so. Those soundness proofs in essence transform a proof of falsity in one system to the other, and relative consistency is the best we can get in order to increase our confidence in a formal system. It is true that traditional model theory, as for example done in [1, 2, 3]. doesn't really foreground the deductive nature of ZFC, it's taken for granted, and reasoning proceeds at a more informal level. If you want to mechanise those proofs, you will have to go back to deduction.
[1] W. Hodges, Model Theory.
[2] D. Marker, Model Theory: An Introduction.
[3] C. C. Chang, H. J. Keisler Model theory.
There is no impenetrable obstacle if humans could do it (for some definition of "could"), but the difficulty is handling infinite state spaces. Model checkers can do it in some situations, but the could do it in more. Neither model checkers nor humans can handle infinite state spaces -- or even very large ones -- in all situations (halting problem and its generalizations).
> Model theory is not some magical deduction-free paradise.
I just pointed out that some of the most successful automated methods, like model checkers (hence their name, BTW) and SAT solvers (which are really special kinds of model checkers), work in the model, not the proof theory.
> The reason we care about model theory in logic is because we want to have evidence that the deductive system at hand is consistent.
The reason we care about models is that we want to know that the "symbols game" of formal logic corresponds to mathematical objects; i.e. that it is sound -- a stronger property than consistency. The model existed first. Proof theory in deductive systems -- and formal logic in general as we know it -- is a 20th-century invention (well, late 19th but only accepted by mathematicians in the 20th).
I gave an example of increasing correctness in the context of record data types, something almost every business app does.
> The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods.
And these are good alternatives for some classes of problem, but how would I use them to type check a SQL query?
> There are easier ways, like Java's permission system, that I mentioned elsewhere.
Hmmm I have my doubts that this is really fit for such a purpose, otherwise why are there various efforts to build a deterministic JVM?
A tank is a way of getting people to work faster than walking, a concern that almost all people have, but that doesn't mean we should propose tanks for that purpose. That dependent types could increase correctness doesn't mean they should be added to a language -- unless its goal is research. This is a common problem I see. Say A is some business concern. The question we need to answer to decide whether to use solution B is not B => A but A => B.
What you're saying is that if I choose to use technique X and I want to achieve Y, then this is a way to do it. This is not the same as saying this is a good technique of achieving Y. The logical implication is reversed from what we'd like to find out. At best you're saying if you use dependent types, you increase correctness. I want to know what you should do to increase correctness, and using dependent types might be the worst possible option. The question is not whether dependent types imply increased correctness, but whether wanting increased correctness implies we should use dependent types. In fact, the post cites a case study about dependent Haskell that isn't exactly a glowing review of the feature.
> And these are good alternatives for some classes of problem, but how would I use them to type check a SQL query?
"Type-checking a SQL query" is not a business goal, and if I try to convert it to some goal you may have been referring to, for example, what is a good way to check if there are mistakes of some simple class in a SQL query, then I'm not sure simple testing isn't more than sufficient. Having said that, I like simple type systems, and I think they are also sufficient for that (e.g. there are typesafe SQL libraries for Java).
> Hmmm I have my doubts that this is really fit for such a purpose, otherwise why are there various efforts to build a deterministic JVM?
I don't know what the requirements are so I don't know.
You could use many of the same arguments you’re making against dependent types against most programming language features. Why should a language have generics? Or first-class functions? Or even any kind of static typing whatsoever? Should Java not have added lambdas because it already had anonymous inner classes? You can clearly get by just fine in a lot of business applications without some of these features.
I think we should rather be discussing whether dependent types are useful for relatively simple applications, like providing type-safe database access or REST APIs in a library, rather than looking at them as tools for proving functional correctness. It’s not so clear that dependent types are too complex a solution there, especially if you look at a library like Servant, which already uses some advanced type system features, and which is actually a really practical library that is probably used in production applications as well. A library like Servant might be able to expressed more clearly with dependent types than with a hodgepodge of type system extensions. I think that wanting type-safe REST API access is already an order of magnitude more practical than model checking kernel code.
That's like saying that a tank could get you to work, so some of its uses are practical for civilians. Does the weight of dependent types justify such disproportionate applicability?
> You could use many of the same arguments you’re making against dependent types against most programming language features. Why should a language have generics? Or first-class functions? Or even any kind of static typing whatsoever?
And those arguments would be just true, except that industry languages adopted those features many years after they've been tried in research languages and shown their worth, while industry languages didn't adopt other features (or perhaps haven't yet), because they didn't prove to be the right solutions to big problems. It's perfectly fine to adopt many ideas that are open research questions, but if you do so you can't deny that your goal is research.
> I think we should rather be discussing whether dependent types are useful for relatively simple applications, like providing type-safe database access or REST APIs in a library, rather than looking at them as tools for proving functional correctness.
No, because that's the inverted implication, or "tank" problem again. Just because a tank can get you to work doesn't mean that it should. If you want to achieve goal A, and feature B achieves it, i.e. B => A, you cannot conclude from that that you should adopt B. You're assuming A and B => A and concluding B. That just doesn't follow.
The question we're asking is whether A => B. We're not asking whether dependent types can be put to some practical use -- that's what researchers ask. We engineers ask what solution to our problem we should adopt (usually the least costly one).
OK, I'll bite. If the entirety of your goal is to do Y, you will never write a single test. Why would you write a test? It doesn't "do Y", for whichever Y is producing profit or some other benefit for you.
Real, True Scotsmen understand that how to do Y is important, because it makes sure that they'll be able to do Z tomorrow. Tests are not essential for functional systems, they are essential for maintainable systems.
Types are just tests enforced by the compiler. Every type-level tool that Haskell gives you is just another tool that makes it easier to write tests that actually help prove that your code is still working.
Half the problem with our industry is that no other industry would accept unmaintainable product. Too many practicioners are practically proud of all their rewrites and green-field projects.
Things like “this writes to the database”, “this makes an unbounded query”, “this requires a random number generator “, rather than a nebulous “oh this has I/O” is very powerful and useful for maintaining a system
1. How do you know that?
2. Why?
3. Why is tracking the effects in the type system useful? Even if and where this is important, it could be easily achieved using something like Java's 20+-year-old security manager and with finer granularity (i.e. you can allow code to read or write certain files, connect to certain domains etc.) [1]. Just because you can do something in the type system, doesn't mean you should, as it may not be the best way.
[1]: https://docs.oracle.com/en/java/javase/13/security/permissio...
Why is it done in the type system? Well, because the goal is to have guarantees at compile-time, and this happens to be something that can be expressed in a sufficiently powerful type system.
No, that's no one's goal. The goal is to increase correctness as much as possible prior to shipping. BTW, reducing soundness guarantees is all the rage in FM research these days [1] precisely because soundness has a high cost, and it is rarely needed for non-simple, technical properties.
[1]: https://dl.acm.org/doi/pdf/10.1145/3371078?download=true
- Hoare logic soundly over-approximates
- Incorrectness logic soundly under-approximates
Sound under-approximation is extremely useful when you want to prove that a certain problem must arise in code, rather than may arise. The problem with logic based program verification has often been that your prover could not prove that a program was correct, but, due to over-approximation of traditional Hoare logic, the best you could learn from this failure was (simplifying a great deal) that something may go wrong. That is not particularly useful in practise, since often this is a false alert.
Of course they are, in the logic sense of "sound", and in the same sense that incorrectness logic is sound. A test is a proof of a proposition about a single program behavior (provided that the execution is deterministic). But neither testing nor incorrectness logic are sound in the sense that term is used in software verification, namely as proofs of some explicit or implied universal proposition. In software verification, a sound technique is one that guarantees conformance to a specification over all behaviors (or conversely, the absence of spec violations in any behavior).
In software verification,
a sound technique is ...
I can see how having something more specific for effects than the most generic IO type is the next step on an evolutionary path for languages with an advanced type system. The concern whether or not it is worthwhile then extends to the whole type system.
2. One example: make sure that HTTP routes that are GET will at most just read the DB, not write
3. I actually don’t like that the type system is where this is going into. I want to have some form of static analysis, and this is providing it.
Usable for applications here means that it should be stable (_e.g._ so you can write your research tools in it and as a common language for sharing code examples in the academic programming language research community).
Market share in the greater software development area (outside academia) was not one of its goals.
Do you have research to show a GC is better than manual memory management? That object oriented programming is any better than procedural? Or any of the other thousands of questions you could ask about extant languages today. But for some reason you need rock-solid evidence dependent typing does X before it's worthwhile to be used in an language?
Not exactly -- they're intended to help with reasoning about the structure of programs and hopefully reject the obviously wrong ones. Correctness would still require a more formal system of validation. Whether this is more easily achieved in a language like Haskell is still an open question. The LiquidHaskell team and Synquid project are both very interesting.
In a Haskell program the compiler trivially rejects programs that fail to provide a branch for a missing case.
I can reason about the scope of what a function can do (and what it cannot) based on it's type information.
I can reason about an equation in familiar terms of substitution and composition.
Types don't automatically ensure my program is correct, for some vague notion of correctness.
Either way, it's not a language that's designed to solve a problem for practitioners
If I am right to assume that practitioners are programmers then I have to disagree with the premise here.
I am not a researcher. I write software for factories to help real people I've met face to face solve real problems.
I have solved pragmatic, real-world problems by writing programs with Haskell and it was a productive, novel experience. The feature I recently shipped to production has migrated nearly a million schema-less JSON documents to a well-defined schema, continuously back-fills the new table from an AWS Lambda function when we receive data in the old format, and was largely only possible to do in such a short amount of time because of the features of Haskell's type system. I haven't had a single bug report or failure in 5 months to boot.
To compare: every single Javascript service we've shipped to production in the last three years, despite all of the testing, validation, and effort we put in to getting it right has at least one production error within three months. Tolerance for these failures has to be built into everything we do.
Haskell is not only suited for research. It is used in Facebook and Github. It has plenty of industrial uses and is definitely designed for and with the aid of practitioners. It's development is largely supported by volunteers: practitioners and researchers alike.
It may not be popular but all it takes is one startup to choose it as their basis to change the conversation. The Viaweb team chose Lisp, arguably as obscure as Haskell at the time, and did great work.
As for dependent types the why is simple: we can express richer specifications in the type system. It would enable Haskell to use a uniform language for terms and types. For programmers the simplest, minimal example are sized vectors as types. You can pass around a vector in Haskell that is sized so that out-of-bounds access is not possible. However the size of the vector is opaque at the type level. With a dependently-typed vector you could specify the bounds of the vector your algorithm supports which further reduces cases where a programmer mistakenly uses your function for unbounded inputs. This is only the minimal example but dependently typed languages scale up from there: there are research languages that have implemented full-on interactive theorem provers and libraries that can encode the whole of mathematical research and knowledge in them: Lean and mathlib. I firmly believe this is where programming is going to go. Dependently typed languages are the next step.
I started writing a guide for interested hackers to get started writing real, working programs in a research-heavy dependently-typed programming language called Lean which you can find here: https://agentultra.github.io/lean-for-hackers/
I suggest giving it a shot before condemning Haskell so easily. There's a lot of promise here.
And in my experience, selling Haskell is a lot easier than selling formal verification, fwiw. Hardly anyone uses TLA+ compared to Haskell. And I spend a fair amount of time and energy trying to sell both.
I have used Lean. It's nice and intersting, but not really a useful tool for software correctness intended for use by engineers. You can do some very interesting math with it, though.
> As for dependent types the why is simple: we can express richer specifications in the type system.
Sure, but why? Expressing richer specifications in the type systems also has a significant cost. A language whose goal is not research would likely spend years considering whether this is a good idea or not.
> I suggest giving it a shot before condemning Haskell so easily. There's a lot of promise here.
I have, and I don't think it's bad, I just don't particularly like it, for the same reasons some people don't particularly like Python or Java. I certainly don't think you can't use it for practical applications, but its evolution is, without a doubt, guided by research goals. And when it comes to promise, I don't know how many decades one can reasonably believe that. Haskell doesn't even spread in companies that are already using it, unlike languages that have contributed a significant bottom-line advantage, and it shows virtually no growth after 25 years, in many of them it was highly hyped. I have absolutely no problem with people who like it. Programming language preference is a matter of personal taste; I like Java, Clojure, Eve, ML and Zig, not crazy about Haskell, and dislike Scala, and others like Haskell and dislike the languages I like; it's perfectly reasonable and expected, like taste in music. But you cannot claim it's a language designed for practitioners and yet have its features guided by research questions.
> Sure, but why?
I already explained why.
Why do you even care about Haskell at all?
> Expressing richer specifications in the type systems also has a significant cost.
And everything that has a cost should have a benefit or we would abandon the whole enterprise.
The simply typed lambda calculus will be 80 years old this year, in June. What was Church going after when he published it to the Journal of Symbolic logic? If you go back and read it he was trying to make sense of the lambda calculus. That calculus gave us one branch of computing as we know it but it was not sufficiently expressive enough to make logical statements about different classes of functions: not all functions that have the same shape have the same meaning.
In a similar fashion not all programs are created equal. Given a set of functional requirements by a person we can probably independently write programs that satisfy them. Type theory is simply a means for us to reason about these programs. Whether you write your program that enables you to verify the internal correctness of your programs with respect to the type system used to check it or not doesn't matter one bit to the user of the system. To the programmer however, it can matter a great deal.
Of the programs we could write in languages that don't allow us to verify the correctness of our programs with respect to a particular type theory all we can say is: when I evaluated the program with these inputs at this time, it worked. We can be reasonably certain it will continue to work and it will likely work on more inputs.
Of the programs we write in a language that does allow us to verify the program is logically consistent and sound with respect to a particular type theory is that it is consistent. We would still be obligated to prove that the program meets the specified requirements. But we don't have to worry about whether we forgot to handle a branch, access data that isn't there, over write data we didn't intend to... and a whole slew of things that do plague us in languages without such tools. We can instead focus our effort on proving that we meet the requirements which is a much smaller and more tractable problem.
As an engineer I don't see the reason why theory and research must be separate. I see my work as sitting between both worlds: theory informs application which in turn gives me more problems to inform the direction to go.
> I just don't particularly like it, for the same reasons some people don't particularly like Python or Java.
That's fair, I don't particularly like Java either.
But I don't go into threads about Java and ask Java developers why they bother with it.
Some of the challenges posted by Stephan are legitimately interesting challenges for Haskell programmers. A dependently typed Haskell would, ironically, make Haskell a more simple language and allow us to continue pushing type-driven programming further for many of the benefits I've described. Many of the benefits to these issues have been described in the article.
> it shows virtually no growth after 25 years
I beg to differ. Even after 10 years it has shown a lot of growth. TFA opens with celebrating the advances made in the last decade.
The reason why Haskell isn't as popular as many mainstream languages, if it's so great, is network effects. Javascript is as popular as it is because it was the only language available for a long, long time on a platform many people wanted to write software for. Ruby would not even be on the radar if it wasn't for it's killer app: Rails. I dabbled in Ruby before Rails came along -- it was super obscure -- but no matter how good it was without Rails it would have languished in obscurity, I think. Some languages became popular by sheer force: Java was a solution in search of a problem and Oracle had a war chest to make sure people thought about it. I recall a time with Python was incredibly rare and obscure and had similar network effects to over-come. Haskell doesn't have a company or group of companies pumping millions of dollars into its development, is not a platform exclusive, and so far hasn't had a killer application where it excelled over other incumbents (except perhaps in compilers).
It also doesn't help that many programmers continue to persist FUD about Haskell for reasons I don't understand. Similar to how people feel justified for being contemptuous of Javascript or PHP I suppose.
However if Haskell was the platform-exclusive language of the web for several decades I think this conversation would be completely different.
Haskell is a fine language and the reasons for working on effect systems are good ones and I'm excited to see the results. If you don't get why then try harder to understand the work or find something constructive to say about it. The people working on it are brilliant and have good, practical reasons for it.
That doesn't answer why because you reversed the logical implication. See here: https://news.ycombinator.com/item?id=22140610
> Why do you even care about Haskell at all?
I don't know anything about, say Ruby, so I have nothing to say about it. But Haskell is an interesting and elegant language that I know, and I like to follow its progress. I just think it suffers from a split brain in the community. The language evolves to answer research questions that I'm interested in, yet some go out of their way to present it differently.
> And everything that has a cost should have a benefit or we would abandon the whole enterprise.
Yes, but that brings me to the point in the linked comments. We are interested in the question correctness => dependent types not dependent types => correctness. The answer to why Haskell should add dependent types is that it's an interesting research question, and that Haskell is designed to answer research questions.
> As an engineer I don't see the reason why theory and research must be separate.
They are separate because the concerns of engineers and researchers are vastly different. A researcher studies X and wants to know what X can do. An engineer wants to know the best way of doing Y. Not to mention that out of every 100 things in research, maybe one will ultimately, after years of engineering, will result in a solution engineers need. How do I know which one is it? I love both engineering and research, but the two are very far apart.
> But I don't go into threads about Java and ask Java developers why they bother with it.
If you were interested in Java then perhaps you should. BTW, I didn't ask why people who use Haskell bother with it. They do it for the same reason people use any non-popular language: they like it. I ask what they think the language is and why it is clearly one thing and yet they insist on presenting it as another. Haskell also suffers from a terrible evangelism disease, where its evangelists don't say things like "I really like Haskell, here's why, and perhaps you should to" but also make incorrect empirical claims about things I know a little about, like software correctness.
BTW, HN isn't a forum for Haskell fans, and anyone can say anything, as long as it's reasonable. I don't go to Haskell forums and discuss my problems with its community because I'm not in the target audience of those forums, but I think I am in HN's. This particular post is at the top of /r/Haskell right now, where it's being discussed by an exclusive group of Haskell fans.
But don't take what I write on social media too seriously. I don't. I think Haskell is a perfectly fine programming language, and it rightly has some fans.
Interesting, yes, but I believe it will also have practical benefits for engineers using the language as well.
I hope Haskell will migrate to dependent types because it will unify the language. Some of the more frustrating features of Haskell are due to it having a separate language for types and terms. When people see a huge list of language pragmas and the singleton libraries being pulled out this is what I hear people frequently complain about when they say Haskell is too complicated. If you can remove the barrier between types and terms then most of that added complexity goes away.
A good example of this is Lean. It's implemented in a dependently typed programming language because it unifies types and terms which makes writing the compiler and programs more simple. I think this could also be extended to Haskell.
It will be difficult, and presented as a "grand challenge," because unlike Lean, Haskell has many more libraries and applications that depend on it and we all know how breaking compatibility goes.
> They are separate because the concerns of engineers and researchers are vastly different.
In the twenty some years that I've been fortunate enough to write software for a living I don't believe this is true. I find that in software engineering that research and application inform one another and have a tight feedback loop. I read papers and often I implement them to help solve problems. Often in implementing that research I find feedback to give the authors or I find new problems that require some research in order to solve.
Pure mathematicians have it a bit harder. I lament that John Conway may never live to see the solution to some of the problems he's posed.
But I think we have it pretty good. The logicians have done most of the work for us. And we can implement new theories quite fast.
BTW I'm not saying you can't comment on or criticize Haskell, this is an interesting discussion. I am a little sensitive to people being contemptuous of the hard work others put into Haskell and was probably either misreading your comments or responding to that. For the people that do work on Haskell I think these are the great challenges for us to solve this decade. Algebraic effects have been used in production at Github and elsewhere and there's still work to do to make them shine but it's generally good stuff and moving in a positive direction. Same with dependent types.
Regardless, thank you for being patient. I appreciate your work and your writing here and elsewhere. All the best.
If in the next fifty years more than, say, 3% of programmers will be programming in a language like Lean, I will eat my hat. Take a Haskeller's favorite, simplest "function", id, and look at its Lean definition (as you know the universe polymorphism is required for consistency):
universe u
def id {α : Sort u} (a : α) : α := a
> I find that in software engineering that research and application inform one another and have a tight feedback loop. I read papers and often I implement them to help solve problems.
That's not what I meant, though. Of course research and practice enrich one another. But their goals and concerns are drastically different. It is rarely the case that an interesting research question is a recommended practice for practitioners. In fact, the more interesting something is to a researcher, the less likely it is to be a good idea for a general recommendation for practitioners.
You're not even putting any stakes on the table. That's such a safe bet. It's unlikely you'd even have a chance at losing the odds are so stacked.
There's a great talk on why functional programming is not the norm: https://www.youtube.com/watch?v=QyJZzq0v7Z4
The short of it is: network effects. Haskell, OCaml, SML... they've never had the benefit of being the exclusive language to a popular platform like the web, macOS, or UNIX. They've not yet had a killer app like Rails or Numpy/SciPy/PyTorch. They've certainly not been foisted on the market with a war chest of marketing dollars like Java and C#. And they're not an incremental improvement on the status quo with an obvious, easy benefit.
> Now, try to explain to a programmer what kind of object id is
That's a rhetorical exercise. You can take a random snippet of APL or Fortran and the outcome would be the same. Every language requires training and effort to learn.
I teach people Haskell and TLA+. If you think teaching people the value of a language like Haskell is hard you should see the blank stares I get on the first day teaching experienced developers TLA+. Interested folks will come around eventually and have their moment but it takes training and dedication to get there.
> was chosen not with the best interests of programmers in mind
I'm well aware. I converse regularly with the maintainers of mathlib and the community. I know the focus there is on building a good tool for mathematicians.
I still think they built an interesting programming language even if that wasn't their intended purpose. That's why I started writing the hackers' guide. The documentation on the programming side is missing and needs to be filled in. They still need programmers to build the tools, the VM, the libraries, etc.
It's niche. And I'm not even the least bit surprised you find it horrible. I don't expect Lean to take off with programmers. I think the ideas in it are good and there is definitely some good things we could take from it in designing the dependently typed programming language that does penetrate the market and over-come the network effects.
Either way I think the people proposing the challenges for Haskell programmers to solve have a good reason to do so otherwise we would have a hard time finding the motivation for it. We want to see where algebraic effects go because new users often complain that monad transformers are hard to learn and users of mtl cite many problems that a well-done algebraic effect system would alleviate. Dependent types would remove the complexity of writing programs that work with types and enable us to write more programs with more expressive types. If you don't see why that's useful then what do you think the community should be focusing on?
It's a great talk in the sense that it satisfies people who want excuses. The real reason is similar to the one in the talk, but more disappointing: over decades, functional programming was not found to be either significantly better or significantly worse than other paradigms in productivity or other similar metrics, but for many years imperative paradigms enjoyed a significant benefit in runtime performance, and so there's really no reason to switch. I honestly couldn't care -- I like, and hate, OOP and FP equally -- but paradigms exist to serve practitioners, not the other way around.
One thing is clear: you cannot at once say you're interested in serving the research of typed lambda calculus -- a worthy research goal -- and also in advancing the state-of-the-art in the software industry, which is another worthy goal, but a very different one. If you're interested in the latter you must conduct some sort of study on the problem at hand; if you're interested in the former, then you have zero information to make a claim about the latter. In other words, you can either want to advance programming or advance typed FP; you cannot do both at once, because doing they both require very different kinds of study. If you're for typed FP, then that position is no less valid than being for OOP, or any other paradigm some people like, but it's not more valid, either.
> And they're not an incremental improvement on the status quo with an obvious, easy benefit.
... or at all.
> That's a rhetorical exercise. You can take a random snippet of APL or Fortran and the outcome would be the same.
I totally disagree here. Simplifying ideas makes you understand what is essential and what isn't, and is absolutely required before some idea can get out of the lab and become a useful technology in the field. If the most basic subroutine represents some object in a meta-universe, that even 99% of mathematicians have no clue about -- you're off to a bad start with engineers. The use of constructive type theory as a foundation is interesting to logicians who want to study the properties of constructive type theories and of proof assistants based on them. It is nothing but an unnecessary complication for software developers. As you point out, there are often some necessary complications, so there's really no need to add unnecessary ones.
BTW, you mentioned TLA+. TLA+ also requires some effort, although significantly less than Lean (or Isabelle, or Coq), but TLA+ has made a historical breakthrough in formal logic. From its inception in the late 19th century, and even from its first beginnings in the 17th, formal logic aspired to be a useful tool for practitioners. But time and again it's fallen far short of that goal, something that logicians like John von Neumann and Alan Turing bemoaned. AFAIK, TLA+ is the first powerful (i.e. with arbitrary quantification) formal logic in the history of formal logic that has gained some use among ordinary practitioners -- to paraphrase Alan Turing, among "the programmers in the street" (Turing said that formal logic failed to find use for "the mathematician in the street," and tried, unsuccessfully, to rectify that). It was no miracle: Lamport spent years trying to simplify the logic and adapt it to the actual needs of engineers, including through "field research" (others, like David Harel, have done the same). That is something that the logicians behind other proof assistants seem to be uninterested in doing, and so their failure in achieving that particular goal is unsurprising.
> Every language requires training and effort to learn. ... Interested folks will come around eventually and have their moment but it takes training and dedication to get there.
But why get there at all? I'm interested, I learned some Haskell and some Lean, I think Haskell is OK -- not much better or much worse than most languages, but not my cup of tea -- and Lean is very interesting for those interested in formal logic, but offers little to engineers; I enjoy it because I'm interested in some theoretical aspects. But why would I subject other developers who aren't particularly interested in a certain paradigm to suffer until they "get there" just for the sake of that paradigm? Again, paradigms exist to serve practitioners, not the other way around.
> If you don't see why that's useful then what do you think the community should be focusing on?
I think the community should be honest about what Haskell is: a testing ground for ideas in the research of typed functional programming. Then, it should consider measuring some results before disappearing down its own rabbit hole, where it's of little use to anyone. Algebraic effects could be an interesting experiment at this point. I don't really care about the pains of all 300 Haskell developers with monad transformers, but if Haskell tries another approach to IO, then it might eventually find a generally useful ones; same goes for using linear types instead of monads. But dependent types? They're currently at the stage when even their biggest fans find it hard to say more good things about them than bad. If Haskell wants to serve software by testing out new ideas in typed functional programming, I think it should at least focus on ones that might still be in the lab but are at least out of the tube.
I will bet you 100 USD that TLA+ had less than 10% of the users of Z before the AWS paper.
> It was no miracle: Lamport spent years trying to simplify the logic and adapt it to the actual needs of engineers, including through "field research" (others, like David Harel, have done the same). That is something that the logicians behind other proof assistants seem to be uninterested in doing, and so their failure in achieving that particular goal is unsurprising.
I will bet you another 100$ that the success of TLA+ has nothing to do with making it "accessible" and everything to do with AWS vouching for it. If reaching the actual needs of the engineers was so important, why is the CLI tooling in such a bad state?
Amazon may not have used TLA+ if not for TLC, but very good model checkers have existed for decades, have been used successfully in industry, and still have not made any inroads into mainstream software.
> If reaching the actual needs of the engineers was so important, why is the CLI tooling in such a bad state?
For one, resources are limited. For another, you assume that the best place to invest effort in order to help developers is in CLI tooling. I, for one, disagree. I think building a model-checker that works well is a higher priority; I also think that designing what is possibly the first "utilized" logic in the history of formal logic is also more important. Even with those two, there are other things that I think deserve more attention, because I think TLA+ has much bigger problems than how you launch some program.
I also think that some of the complaints about the tooling might be about something else altogether, but I'm not entirely sure what it is. Simply doing what beginners think they want is rarely a good strategy for product design. You get the feedback, but then you have to understand what the true issue is. Having said that, there can certainly be some reasonable disagreement over priorities.
What I'm saying is that either TLA+ wasn't the first (Z was earlier), _or_ TLA+'s success has much less to do with anything especially accessible about it and more because a high profile company wrote about it.
> because I think TLA+ has much bigger problems than how you launch some program. [...] I also think that some of the complaints about the tooling might be about something else altogether, but I'm not entirely sure what it is. Simply doing what beginners think they want is rarely a good strategy for product design. You get the feedback, but then you have to understand what the true issue is
When I asked "what would make TLA+ easier to use", tons of people mentioned better CLI tooling. You told them all that they don't actually need that and they are thinking about TLA+ wrong. Maybe you aren't actually listening to the feedback.
I've also heard it from tons of experienced TLA+ users that they'd like better CLI tooling.
Was Z ever used outside high-assurance software (or the classroom)? BTW, while Z certainly employs a formal logic, I don't think it is a formal logic itself -- unlike TLA+ -- at least not in the common usage of the term.
> TLA+'s success has much less to do with anything especially accessible about it and more because a high profile company wrote about it.
But for a high-profile company to write about it, it first had to be used at that high-profile company for some mainstream software. My point is that being an accessible logic may not be a sufficient condition for adoption, but it is certainly a necessary one, and an extraordinary accomplishment. Both Isabelle and Coq have had some significant exposure, and yet they are still virtually unused by non-researchers or former researchers.
> When I asked "what would make TLA+ easier to use", tons of people mentioned better CLI tooling.You told them all that they don't actually need that and they are thinking about TLA+ wrong. Maybe you aren't actually listening to the feedback.
Maybe, but "listening to feedback" is not the same as accepting it at face value. The vast majority of those people were either relative beginners or not even that. To understand the feedback I need to first make sure they understand what TLA+ is and how it's supposed to be used, or else their very expectations could be misplaced. I've written my thoughts on why I thought the answer to that question is negative here: https://old.reddit.com/r/tlaplus/comments/edqf6j/an_interest... I don't make any decisions whatsoever on TLA+'s development, so I'm not the one who needs convincing, but as far as forming my personal opinion on the feedback, what I wrote there is my response to it. It's certainly possible that either my premise or my conclusion is wrong, or both. It's also possible that both are right, and still better CLI support should be a top priority. That is why I would very much like to understand the feedback in more depth. If you like, we could continue it on /r/tlaplus (or the mailing list), where it will be more easily discoverable.
> I've also heard it from tons of experienced TLA+ users that they'd like better CLI tooling.
Sure, but the question is, is that the most important thing to focus efforts on? Anyway, I'm sure that any contribution that makes any part of the TLA+ toolset more friendly, even if for a subset of users, would be welcomed and appreciated by the maintainers, as long as it doesn't interfere with what they consider more important goals.
The state of the art doesn't advance until practitioners share the results of adopting new techniques and tools. How else would the SWEBOK guide [0] have a section on unit testing if, in study, we don't have results that correlate the practice of TDD with a reduction in software errors, productivity, or some form of correctness? Is it irrational of us to practice TDD anyway?
How do we know formal methods are effective if there hasn't been a large scale study?
An interesting example of this balance between research and practice came to me from learning about the construction of cathedrals, particularly the funicular system of Guadi [1]. Instead of conventional drawings he used hanging models of the structures. It was not widely practiced or a proven method but it enabled him to reduce his models to 1:10th the scale and accurately model the forces in complex curves. As he shared his work and others studied it the state of the art advanced.
> .. or at all.
> I think Haskell is OK -- not much better or much worse than most languages, but not my cup of tea -- and Lean is very interesting for those interested in formal logic, but offers little to engineers
I think we're at, or approaching, the point where we're talking past each other.
I heard the talk from the Semantic team at Github on their experience report with algebraic effects sounded positive [2]. They are probably the largest production deployment of a code base exploiting algebraic effects. Their primary area of focus is in semantic analysis of ASTs. And yet they would like to continue pushing the state of the art with algebraic effects because, in their words, In Haskell, control flow is not dictated by the language, but by the data structures used. Algebraic effect interpreters enable them to interpret and analyze unsafe code without having to maintain buggy, difficult to reason about exception-based work flows. They say this singular feature alone is essential for rapid development.
Yes, they're doing research. However their research isn't in answering hypothesis about effect interpreters. It's directly contributing to an interesting feature in one of the largest code-sharing platforms in the world. They were able to exploit algebraic effects so they could focus on their research, their real-world problem, without having to fuss around with the limitations of conventional mainstream languages.
I do wish more companies using Haskell would share their experiences with it. It would go a long way to dispelling the pervasive view that Haskell is only good for research. It's not: it's a practical, production ready language, run time, and ecosystem that can help anyone interested in using it to tackle hard problems.
In a similar fashion I think dependent types would make working with types in Haskell easier. Instead of having to learn the different mix of language extensions you need to enable in order to work with inductive type families, it could be more like Lean, where it's a normal data declaration. Haskell introduces a lot of extra concepts at the type level because it has two different languages. I can simplify a lot of code in libraries I've written if Haskell had dependent types (and I'm working on libraries in Lean that may eventually prove it).
It may take a while but I think Haskell will eventually get there. The community has been discussing and researching it for years. It's going at the pace it is because the Haskell community is not focused on pure research: there are a lot of production applications and libraries out there and they don't want to break compatibility for the sake of answering interesting research questions. Despite your opinions on type theory there's a real, practical reason I might exploit Rank-2 types or Generalized Algebraic Data Types and it's not simply to answer a pressing hypothetical question: I've used these in anger.
I hope some of this answers your questions as to why get there at all?
[0] https://www.computer.org/education/bodies-of-knowledge/softw... [1] https://en.wikipedia.org/wiki/Church_of_Col%C3%B2nia_G%C3%BC... [2] https://github.com/github/semantic/blob/master/docs/why-hask...
As to Haskell, it is definitely production-ready, and usable in a variety of circumstances. Also, its design and evolution are just as definitely primarily guided by research goals. These two simple, obvious, facts are not in opposition to one another. I have read numerous articles on why some people like Haskell, or many other languages. They are very important: some people like the tracking of "side effects"; some enjoy the succinctness. None of those articles, however, have any bearing on other questions. Which are not necessarily more important, but they are very different.
Lean. It's implemented in a
dependently typed programming
Anyway, nobody doubts that Lean's logic is a dependently typed formalism: "Lean is based on a version of dependent type theory known as the Calculus of Inductive Constructions" [1]. I thought the discussion here was about using dependent types in programming languages. Note that logics and programming languages are not the same things.
[1] J. Avigad, L. de Moura, S. Kong, Theorem Proving in Lean.
I meant that Lean, I think, could be implemented in Lean.
Do you also work with Lean?
I'm not currently working with Lean, but I will start a large verification project in a few months. We have not yet decided which prover to go for. We may write our own.
remove the barrier between
types and terms then ...
Edit: I forgot about consultancies like Well-Typed and Tweag
Another trend (that I don't particularly like) is all the blockchain startups using Haskell.
All of the pretension that comes with knowing one of the functional languages that has a community that pretends to know math, and they end up working retail. Ow.
Joking diss aside, though, I definitely feel for people who love languages with limited reach.
(Also, I think GitHub hired a few people explicitly for Haskell, which is worth mentioning because Microsoft is vaguely more reputable than most of the companies listed in this thread.)
the act of trying to appear or sound more important or clever than you are
Some irony in your comment. I meant exactly what was said.
https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
(Or really, just combine "cryptocurrency" or "cryptocurrencies" with any negative word and throw it into search and you'll see the point.)
All cryptocurrency has a serious reputation problem right now, and it's probably not going to go away for the considerable future.
It doesn't mean that the company has a product.
Sorry but doesn't this statement fit better to the definition of "borderline" something?
I'm not that pro-haskell but I also see how all languages in the last decade shifted toward fp idioms clearly. I mean redux is a fold.
And although a lot of practically useful stuff has come out of Haskell-land (property based testing, for example), it's not even obvious to me that Haskell has been a huge part of the shift to more FP-y idioms (compared, to say, scheme or SML). Your own example, fold, has been around decades before Haskell.
I agree that SML isn't even on the map, in terms of practical programming language choices (one of the most hilariously titled CS books of all time must _ML for the working programmer_ where the final "real project" chapters consist of writing such working programer perennials as a lambda calculus interpreter and a theorem prover). And I believe that even scheme is less suited to write almost any type of practical software than Haskell. But that's precisely my point: a language having a positive influence on the state of applied programming does not mean that it is actually a good choice for solving practical problems with. And vice versa.
btw I love sml. I'm just being realist about it's mainstream existence.
Lastly, it's as if you consider haskell as proof of concept and nothing more. I don't see any real hurdles why haskell is less practical than typescript (except the fact that TS relies on the years of js project they can compile and interop with)
By the way, I'm particularly interested because I am writing about Haskell myths. I have a very rough draft at http://h2.jaguarpaw.co.uk/posts/haskell-myths/
I understand your question though, it's highly possible that the devs picked haskell for their own interest. But so far it's been a few years and the haskell "module" is dealing with the core of their business.
Except that's exactly what languages that provide a business value do (like the ones I mentioned). Maybe not always in all layers, but they tend to fill a big, wide niche at a company very quickly.
Like Brian Goetz puts it, it is not FP vs OOP, rather combining FP and OOP, using the best of each to solve different kinds of problems with the same tool.
FP and OOP are both well tested design patterns. Mixing them up in an incoherent way just makes the whole software architecture somewhat unpredictable.
FWIW, I also don't know that Python officially conceives of itself as multiparadigm so much as as a procedural language with classes. Kids these days forget that higher-order programming has a long history in procedural programming, too. ALGOL was doing it in the 1960s, after lisp but a good decade before Backus published Can Programming Be Liberated from the von Neumann Style?.
I'd say that OCaml blends imperative and functional programming cohesively and fairly equally, though.
How programming paradigms can be lift over to the level of "algorithms + data structures", regardless of the language.
Some problems get better solved as a set of classes, others as functions operating across data alongside pattern matching, and yet others are happy to take lambdas as callbacks.
Many of the anti-OOP crowd doesn't realize how much OOP is already available on Common Lisp, that Smalltalk-80 already allowed for a good LINQ like mix with its blocks and collection methods, or how SML modules can be combined to make what isn't much different from interface based polymorphism.
It is a matter of having a nice toolbox instead of just a hammer. :)
Monads are just one of many ways of formalizing notions of state. All of them have their tradeoffs. For example, in temporal logic it's much more obvious that "state does not compose" due to the frame problem.
And yes, monads are a way to express some non-deterministic computations in lambda-calculus-based languages, as are linear types.
> Haskell's greatest success
Success in what sense? In expressing what amounts to side-effects in a language based on a lambda calculus as monads? Sure.
They are a workaround, because by definition purity implies that nothing changes in the world.
I can run the same Haskell program multiple times, and it might eventually produce different values as output given the same input values, e.g. an URL or file handle.
As @willtim explains, monads were applied to PL theory to model effects. The IO monad models the effect of state, i.e. imperative programs. The type `IO a` is essentially a "wrapper" or "alias" for the type `RealWorld -> (RealWorld, a)`. You should think of the entire world as being the input to a Haskell program.
Haskell does have impure backdoors into IO such as unsafePerformIO, but the IO monad itself is perfectly pure.
P.S. For more information, check out the work of Eugenio Moggi [0], who started using monads to give semantics to programming languages, and Philip Wadler [1], who applied the idea on a programmer-facing level.
[0] https://person.dibris.unige.it/moggi-eugenio/ftp/ic91.pdf
[1] https://groups.csail.mit.edu/pag/OLD/reading-group/wadler-mo...
Researchers who study some technique X ask themselves how best to use X to do Y, and publish a series of papers on the subject, but practitioners don't care about the answer to that question because they don't care about that question at all. They want to know how best to do Y, period. One could say that every language, once designed, is committed to some techniques that it tries to employ in full effect. But any product made for practical use should at least strive to begin with the why rather than the how, both in its original design and throughout its evolution. I work with designers of a popular programming language, and I see them spending literally years first trying to answer the why or the what before getting to the how. So either Haskell is a language intended as a research tool for those studying some particular techniques -- which is a very worthy goal but not one that helps me achieve mine -- or it's intended to provide entertainment for practitioners who are particularly drawn to its style. Either way, it's not a language that's designed to solve a problem for practitioners (and if it is, it doesn't seem that testing whether it actually does so successfully is a priority).
I think it's important to have languages for language research, but if that's what they are, don't try to present them as something else. And BTW, at ~0.06% of US market share -- less than Clojure, Elixir, Rust and Fortran, about the same as Erlang and Delphi, and slightly more than Lisp, F# and Elm -- and little or no growth (https://www.hiringlab.org/2019/11/19/todays-top-tech-skills/), I wouldn't call Haskell a "popular language," as this post does, just yet.