Hacker News Reader

Comment by mikekchar | Hacker News Reader

The really simple answer to this question is: because at a high level of abstraction, it isn't useful. Most applications are being specified by people who don't understand in any detail what they want the application to do. They can't even imagine the problem well enough to discuss it let alone specify it. A very large proportion of failed projects I've seen is due to this break down. The people who have the time and inclination to investigate the details are not the ones who care what it does. You can have an incredibly low defect count and still not build the thing you need.

But if you look at a lower level of specification, then formal methods start making a lot more sense. For example, let's say I have to implement a communications protocol. This is something I can specify and that I can build against that specification. Companies sell protocol testers that test your implementation against a protocol. It might be nicer to have a formal specification than a back end test -- especially because there are often more scenarios you care about than you can feasibly test.

At an even smaller scale, we are now realising some benefits of this mode of thinking. For example, we've had types in programming languages for a long time, but lately we're able to actually make statements about what the code does, simply by analysing the types. This is a massive step forward and I'm really looking forward to things like constrained types making it into the mainstream. Similarly things like Rust's borrow checker can allow you to make analytical statements about how much memory you are using (if you are careful), etc, etc. These are great.

I think that the success of formal methods is going to be through the backdoor and at this design/implementation level for a long time. In fact, pretty much forever.

View on HN

I think you're mistaking the use of formal methods for some particular process (like confusing tests with TDD). Formal methods do not require that you have a specification in advance. They can help you come up with the specification, through interaction, before or during coding (e.g., this is a lightweight formal specification tool for designing UIs and interaction: https://sketch.systems/).

As code is itself a specification at a very low level, you must have some kind of specification in your mind by the time you write it. Is it always worthwhile writing it in some formal methods tool? No, but it certainly can be when there is some subtlety or potential complication, which can arise even in seemingly simple programs. The author of this post has some nice examples here: https://youtu.be/tfnldxWlOhM

It is true that formal methods only help; they don't solve all of your problems, and they certainly can and do result in wrong specifications (e.g. KRACK attack and Spectre/Meltdown are examples of a wrong specification), but that doesn't mean they cannot be extremely helpful, just as unit tests are helpful even if they don't find all bugs.

I have a MSc with a specialization in formal methods from a place with famous faculty in the field, so I might be biased. But I have to disagree with almost anyone here.

Formal methods still lack a bit of maturity and streamlining to get adopted. It's a bit like functional programming in the late 90s and early 2000s. Nothing was terribly different from now, yet it was not widely used. Whereas now, we are starting to see adoption by mainstream players. E.g. lots of features in Swift.

With regards to formal methods, the situation is entirely analogous. The theory is there. Already developed. And it sits at the absolute core of CS. It's all about formally describing semantics. There are several approaches: type systems, model checking, program analysis and abstract interpretation. And these offer a tremendous amount of flexibility. You can go all the way from adding some lightweight formal specifications a posteriori with e.g. a fancy type system, to developing all your code formally by starting with some axioms.

I have a MSc with a specialization in formal methods from a place with famous faculty in the field, so I might be biased. But I have to disagree with almost anyone here.

With regards to formal methods, the situation is entirely analogous. The theory is there. Already developed. And it sits at the absolute core of CS. It's all about formally describing semantics. There are several approaches: type systems, model checking, program analysis and abstract interpretation. And these offer a tremendous amount of flexibility. You can go all the way from adding some lightweight formal specifications a posteriori with e.g. a fancy type system, to developing all your code formally by starting with some axioms.

> You can go all the way from adding some lightweight formal specifications a posteriori with e.g. a fancy type system, to developing all your code formally by starting with some axioms.

This statement particularly interested me. If I wanted to learn more about this, what resources do you recommend?

If you ask how deep I want to go, let's say we have a scale of abstraction that's from 1 to 10, where 1 is a two paragraph executive summary and 10 is an entire Ph.D's worth of training. I'd probably be looking at a 2.5 to a 5.

Some references below. You'd probably want to start with the first 3. The other 3 are classics, but much more dense (e.g. the Nielsons book requires some decent abstract algebra background):

* Software Foundations (Pierce): https://softwarefoundations.cis.upenn.edu/

* Concrete Semantics (Nipkow): http://www21.in.tum.de/~nipkow/Concrete-Semantics/

* FRAP (Chlipala): http://adam.chlipala.net/frap/

* Model checking (Katoen): https://mitpress.mit.edu/books/principles-model-checking

* Program analysis & abstract interpretation (the Nielsons): https://www.springer.com/gb/book/9783540654100

* Type systems (Pierce): https://www.cis.upenn.edu/~bcpierce/tapl/

Judging by the reading list you've provided below, you may not be familiar with more "productized" formal methods, designed for use by working engineers, like TLA+ and Alloy. I don't know if I'd call them entirely "mature" yet, but they are certainly industrial-strength, learned by ordinary programmers in 2-3 weeks of part-time reading of tutorials or in a few days with guidance, after which they go on to specify and verify large, complex real-world systems.

Lamport spent years simplifying TLA+ and designing it for user-friendliness (at the cost of making it inappropriate for logicians to do research on novel logics). While extremely powerful (people have implemented TLA in Isabelle and Coq to reason about concurrent and interactive systems), it is based mostly on ordinary, high-school or first-year-college math, and entirely eschews the complications of programming language semantics.

See the following industry reports:

* Amazon: http://lamport.azurewebsites.net/tla/formal-methods-amazon.p... -- this has been so successful that managers encourage developers to use TLA+ to reduce development costs.

* Microsoft: https://youtu.be/ifFfxRCX_jw

* https://youtu.be/tfnldxWlOhM

Completely agree. This line sums it up:

>> Before we prove our code is correct, we need to know what is “correct”. This means having some form of specification

That is the problem. The people who come up with the spec don't fully know what is required. It's even worse than that actually; the requirements change constantly to account for changes in the technological and business environment within which the project exists.

The people who come up with the spec don't fully know what is required. It's even worse than that actually; the requirements change constantly to account for changes in the technological and business environment within which the project exists.

I think this is a bit of an overstatement, because it implies an often unrealistic separation between writing specs and writing implementations. There may be several levels of each, and the middle levels may overlap.

For example, it may well be the case that the management on a project don't get heavily involved with the technical details and just specify "A needs to communicate with B" as part of the high level requirements. That doesn't mean the technical people responsible for implementing those requirement won't specify detailed protocols at a lower level and wouldn't benefit from formal methods to help ensure correct implementation.

think this is a bit of an overstatement, because it implies an often unrealistic separation between writing specs and writing implementations

Every government IT project that is years late and billions over budget is because of this

> Every government IT project that is years late and billions over budget is because of this

Well, that used to seem to be true before governments started experimenting with (methodologies which were notionally versions of) Agile, Lean, and related ideas. Then there were a whole new set of reasons for IT projects being years late and over budget.

False. Writing a waterfall-style “spec” on paper has nothing to do with formal methods.

It absolutely does. We studied SSADM in college.

> it implies an often unrealistic separation between writing specs and writing implementations

I think that part of the problem is that small modification in the spec can lead to enormous changes in the proofs

I think it's worse than that.

I did a course on formal methods at university. The 'spec' ended up being a lot more complicated than the actual program.

I wasn't really confident afterwards that the "proved" software actually did work.

I think it's possibly a suitable method for building very low level code (e.g. sorting methods) where the spec is going to be exceptionally simple but it's effectiveness drops off quickly the higher up the stack you go.

I had exactly the same experience. We did specification in Z, but the code that was supposed to be "proved" correct was a clearer reflection of what we wanted to do than the "spec".

So I actually had more confidence in the code than I did in the spec.

And I think this answers the question of the OP: people don't use formal methods because

(a) the vast majority of problems don't start out with a formal spec

(b) the gap between informal and formal is vastly more relevant than the one between different formalisms

And yes, when you have a sub-problem that is mostly formal, then it can make sense, particularly if there's a lot riding on it.

> And I think this answers the question of the OP

Do you realize that the OP is actually linking to an article explaining this (and a bunch of other aspects) in great detail?

While it's a good article, I didn't see it covering this aspect, particularly (c).

Would the code have been as clean and clear if you did not make the formal spec beforehand?

Yes

That's a problem with specs, the most concise and complete way to write them is by writing your program. If it wasn't, people would just compile the specs, and program using those.

Now, go tell this to people that want to offshore development based on a spec... But that's a digression.

You don't prove correctness of an entire program against the entire spec. That's only possible with toy problems, even entirely proved programs (like secL4) only prove some point of view, never the entire spec. Some times in a large program you discover a property that is very important (like how to assembly some event set into data, lack of deadlocks in a distributed system, or lack of buffers overflow), you then go and prove those properties.

> That's a problem with specs, the most concise and complete way to write them is by writing your program.

I've never dealt with formal specs/design, certainly nothing like those described here. Your comment (however in/accurate) strikes me as interesting and leads me to wonder...

What if we took the code and processed it to generate a "spec"? (I quote "spec" here b/c I wouldn't consider it a spec, but don't know what else to call it.) Basically, a document that explains verbosely what the written code does... hopefully in a way that is reasonably, humanly digestable.

Then we might get a doc that says, "Function add(...) accepts two integers/nulls and returns the sum." And Joe-coder looks and realizes it shouldn't accept nulls, goes back to the code, fixes the issue.

If there was a rule that functions could only return named variables (vs expressions that evaluate to a value that is returned) it would get closer to "this function accepts paramName1 and paramName2 and returns sumOfParams".

This is essentially what static code analysis attempts to do. Unfortunately, there are many ways of writing programs that today's static code analysis cannot understand.

I think the issue with the way people try to promote the use of formal methods, is that they assume that people will want to model their system formally before implementing it.

I feel like there'd be more productivity in showing people what their code could do, and helping them narrow that down to what it should. It is, of course, hard to do this.

From this point of view I like TLA+, it gives you a simple but powerful programming language and then allows you to check stuff like "this must not happen" or "this must happen" (and more).

Formal proof as in coq-proof are often not reasonable for many dynamic projects

Indeed, I've never in my career (in high level businesses, I.e. Finance, advertising) seen such a thing as a proper 'specification'.

It's more the business has a high level, rough idea of a change/feature to improve the business, and we figure out together the exact details, some of which surface during implementation, and then verify it gradually in the wild.

We could have spent x10 time instead drawing up a formal spec up front, but it would have so many assumptions baked in, that it'd get invalidated in the wild anyway.

So the people designing the spec don't have enough information about the problem space. As the programmers begin working, they explore the problem space, extract the information they need to understand a solution, and then they can actually solve it. Bit of a Schrodinger's cat situation... The solution must remain undefined until observed.

But if you write some code, you must be writing it to do something. That something is your spec. This may or may not be what the customer wanted, but writing it down may make it easier to explain what it is that you've decided to implement, and understand whether or not it could be the right thing.

Requirements do change constantly, which is all the more reason to write specs, so that you can understand the change and its implications (and present it to your customers) before writing the code. I am not saying this is always the best approach, but changing requirements in itself is not a reason not to use formal specification, but an additional motivation to use them.

For example, this is a nice lightweight formal specification tool that allows to specify UI interactions quickly and play with them to see if they are satisfactory before implementing them: https://sketch.systems/ This is more "agile" than changing code between iterations.

There is a substantial language barrier; articles like this keep using the word 'proof', and I can't figure out what they mean.

Each discipline has it's own standards of proof. In mathematics, the word means that a statement transcends the laws of time and space. In law, it means a group of 'reasonable people' can be convinced. In science it means that there is a theory with supporting data that has not been falsified. I'm pretty sure to the historians it means a tenured professor thinks it makes a good story.

Whatever the word means applied to computer science, it does not mean:

1) That the thing proved actually works (it can be proved correct, and still have bugs)

2) That the thing proved does what you want (extensively discussed here, the spec can be wrong)

3) That the thing will be useful (also extensively discussed; and I'd add that protocols like TCP, for example, seemed to get adopted because it was so simple anyone could understand it, it isn't obvious that being provable makes it more robust to network errors)

When I see people getting excited that they have prooven tail has types [a] -> [a], all I can think of is that some programmer will make "a" some sort of super object at the root of an object hierarchy, and then what on earth is being gained?

It is more obvious for cryptography applications why proofs might be valuable, but I suspect any data showing formal methods outperform more testing generally is really just identifying that design and scoping studies add value, and nothing to do with the merits of whatever 'proof' means here. 'Proof' might just mean that you have someone who can't communicate ideas in simple English and is going to give you a page of esoteric notation.

Proof in formal methods means the mathematical kind: with certainty the program / function implements the specification.

Mathematicians can also prove something irrelevant or useless, or something fundamental like 1+1=2.

Well, yes, but if mathematicians prove something then we know it is true. And if they can't prove the trivialities, that would be a crisis for the entire discipline, because 1+1=2 relates to everything they do.

If software people prove something we also know it is true, but not that it usefully relates to the software. In fact, 0.1+0.2 is likely != 0.3 for most software. You can prove you have integer types or fractional types or whatever, then a hardware bug comes along and your proof doesn't relate to the real world anyway. So what exactly is the standard we are working to? Is proof reasonably superior to more effort testing? That is a debatable point, and the economics suggests no.

Since formal methods are clearly targeted at programming, what is this link to software? We can prove trivial things like 1+1=2 but that still doesn't necessarily connect to anything that gets implemented.

Any program is a trivial proof of itself; so why are we interested in these specific proofs? Saying that they have a proof doesn't seem meaningful and is a language barrier to whatever they actually mean - which having had a good long think, is probably 'programmatic scoping', which describes what they actually seem to be doing.

Although it is not self evident from looking at most modern software, prgogramming and proofs are (in some instances) direclty related by the Curry-Howard correspondence. Apart from such instances one can also try to assert temporal relationships between variables in a program that have to hold under all inputs (one example would be “valid until ready”, which is a typical requirement one would have for a queue interface: the producer can not revoke the claim that the data is valid until the consumer has accepted it). Such assertions can be verified with TLA+ or in System Verilog with tools such as Formality.

> You can prove you have integer types or fractional types or whatever, then a hardware bug comes along and your proof doesn't relate to the real world anyway.

Proofs always rely on some sort of axiomatic system. Otherwise you don't have any basis for starting deductions. In most cases "the hardware conforms to its spec" can be considered a reasonable axiom (unless maybe in space flight where cosmic rays may cause appreciable amounts of random behavior).

This is fundamentally a complaint about some fairly specific language use. A lot of articles I've seen talking about formal methods contain some varient of "rigorously verified the correctness [of the program]". Anyone who is half-unsure about what is happening is going to write that off, because we all know programs can't be formally verified as correct in the common meaning of 'correct' because bugs are everywhere, at every level of the stack, and what people ask for probably isn't what they wanted anyway.

That is an abuse of language. What is happening is (and this is a good article because it is quite clear on the point) that "We’re ... prov[ing] ... conform[ance] to some spec.".

Now I'm quite excited at the prospect of automatic checking of conformance against a spec. Looking foward to the non-alpha release of spec in Clojure, in fact. But I'm going to ignore anyone who talks about "proving correctness" on the assumption that they (a) can't prove a program is correct in the abstract, (b) sound pretentious and (c) I'd be worried they are more worried about proving things than scoping and testing which is where most of the value sits.

Basically, I'm not saying formal methods are bad; quite the contrary; but the word 'proof' is not a safe word. It means very different things to different people. Most people outside software would surely assume bugs in the spec disprove 'correctness', but that isn't what the language seems to mean to formal methods people.

> the hardware conforms to its spec

Not a safe assumption. Spectre and Meltdown happened just last year; and I assume caused a lot of programs which were required to be high-certainty to become uncertain in practice.

The Software Engineering implications of a 'proof' are _different_ from a mathematician's standard of proof. If a mathematician uses a prooved fact, as long as the proof is correct then they have certainty. If an engineer uses a prooven program, they still don't have certainty because they are working in the real world.

I've opened news.ycombinator.com in firefox quite a few times over the years; every time I've either gotten the web page or a network error. That is a proof of correctness to the standards of 90% of the academic disciplines.

> So what exactly is the standard we are working to? Is proof reasonably superior to more effort testing?

Empirically, yes it is (see e.g. "Finding and understanding bugs in C compilers"). Testing can show the presence of bugs, proofs show the absence of (a class of) bugs. This is a worthwhile exercise, even if your model is not perfect.

This is not an all-or-nothing proposition. There are lightweight forms of formal specification and proofs which you are probably already using. One example are types. If your program is well-typed it might still crash with a division by zero or some other runtime error, but it will not crash because you tried to execute code at address 42 after you mixed up your integers and code pointers.

> In fact, 0.1+0.2 is likely != 0.3 for most software.

This seems like a rather silly example: you're presumably talking about floating point numbers, but we have a spec for floating point, it's IEEE 754. This spec has been formalised in many proof systems, e.g. (top Google hits for various systems I know):

  https://github.com/coq-contribs/ieee754

  https://agda.readthedocs.io/en/v2.5.4/language/built-ins.html#floats

  https://www.isa-afp.org/entries/IEEE_Floating_Point.html

I'm tempted to say that using integers/rationals/reals in a proof, when the software uses 64bit words and floats, is a rookie mistake; yet I've never even seen rookies make that mistake. Maybe that's a problem for approaches which keep programs and proofs separate, but in systems based on type-checking (e.g. Agda and Coq) it wouldn't even be possible to make such a mistake (there's no way to use different types in the program and the proof, since the program is the proof).

> You can prove you have integer types or fractional types or whatever, then a hardware bug comes along and your proof doesn't relate to the real world anyway.

I'd be very happy if hardware bugs were the main cause of my software's problems ;) More seriously, this seems like moving the goalposts from "is it useful?" to "is it perfect?".

> In mathematics, the word means that a statement transcends the laws of time and space. In law, it means a group of 'reasonable people' can be convinced.

This was historically and still is largely false. A mathematical proof is a written argument and most proofs are too complex to be "obviously correct", therefore mathematical proofs are usually more like your latter case: It is an argument that convinces people. Mathematics has a long history of doing things "that sound right but haven't been proven yet but it seems to work out ok", e.g. this was done all the time in the earlier days of analysis.

Computer science is a branch of mathematics, so proofs are of the mathematics kind.

Formal proofs will prove whatever you designed them to prove. It may be that #1 of yours, or the #2 if you actually know what you want (AKA "never"). Your #3 is mathematically ill defined, and math can not prove ill defined statements.

> When I see people getting excited that they have prooven tail has types [a] -> [a], all I can think of is that some programmer will make "a" some sort of super object at the root of an object hierarchy, and then what on earth is being gained?

I don't really understand that question. The type means that whatever list you pass that tail function, you'll get a list of the same type back. That's information you can decide to use to build your program, or just ignore. Without further context, there isn't any defined value for that information.

> The really simple answer to this question is: because at a high level of abstraction, it isn't useful. Most applications are being specified by people who don't understand in any detail what they want the application to do.

The world is changing.

In high-growth-potential areas, I think we're starting to see a shift away from the style of software where "what to build is hard but how to build is easier" and toward application domains/products where exactly the opposite is true.

IoT, next-gen factory automation, robotics, ADAS, automated trading, etc. all have two extremely important things in common:

1. It's really obvious what we want the system to do (minimize energy usage; produce widgets without killing Joe the machinist; go to the store and don't kill anyone; make money; etc.)

Unlike with social apps/online communities/productivity software/games, the "what did the customer want" problem is likely not THE key failure point.

2. It's extremely non-obvious how to map those high-level desires onto software.

These application domains, which I think will drive growth in the software industry during the next cycle, are kind of dual to our current ones (web and mobile apps).

So, at the highest level of abstraction we know what the customer wants. That's not the point where we need the most derisking. Also, the hardest problems -- the ones where derisking efforts will land -- are amenable to mathematical treatment. Because of this shift, mathematical modeling tools are going to play a big role in the industries that (I think) will drive growth in the coming decades. And that means the zeitgeist of software engineering will change.

I'm not sure if those mathematical modeling tools will look anything like today's theorem provers and model checkers. Probably only in the same way that Python looks like FORTRAN.

> shift "what to build is hard but how to build is easier" toward application domains/products where exactly the opposite is true.

Interesting insight, thanks for sharing. I wonder how this will affect management of teams that deal under these conditions.

As a counterpoint to that, another change happening in the industry now is the increasing tendency to delegate more and more to ML models, which are even less amenable to formal verification than mainstream PLs.

Absolutely, but why would that preclude formal methods?!

In fact, this is exactly what I was thinking about when writing the last paragraph of my comment.

You can prove the ANN works, but how do you check it conforms to any specification, other than by testing and accepting high probability of real world failure?

Eventually, you have a high level fuzzy requirement which is hard to even specify right. Just look at, say, latest YouTube guidelines about content they try to ML around to make tractable...

And that's a classifier, now try to do the same with a machine translation system.

There are papers that use SMT over RNNs to prove smoothness of the output functions. You can absolutely apply these techniques to ML.

So you have any links? I’m very curious, and a quick search did not turn up anything.

Clark Barrett's group at Stanford (previously NYU) is a leader here.

Thank you!

I'm not buying it; I believe the problem is more on the human side.

"Most applications are being specified by people who don't understand in any detail what they want the application to do", because most humans absolutely suck at clear communication and clear thinking. They're not aware what they're not communicating. They're not aware what scenarios they're not considering. Examples abound - remember that time where your spouse/parent asked you, "go to shop and buy milk", and you knew you now had to drill them for things like "when", "which shop", "which milk (%/brand)", and "what other %/brand is OK if the one you're looking for is sold out", because they'd be unhappy if you did the wrong thing? Most people who don't work with actual STEM, programming or law seem to be like that, almost completely unable to articulate in a clear and complete way, and completely unaware of how much they're not communicating.

> 1. It's really obvious what we want the system to do (minimize energy usage; produce widgets without killing Joe the machinist; go to the store and don't kill anyone; make money; etc.)

This is not "obvious" and is a good example of an unclear specification. The "not kill Joe" may be an implicit assumption shared by all moral people, but at some point it'll have to be quantified, e.g. for risk analysis, and the question "how low probability is low enough" will pop up. "Minimize energy usage" is limited by goals and tradeoffs that need to be stated; I can make you a sensor run a decade off a coin battery, but there's a good chance that's not what you want. Etc. Etd.

Circling back to the GP's statement, does the customer who wants the energy-efficient, safe, money-making contraption understand enough about either requirement to do a formal specification on it? I believe they do not, and it's the same situation as with cat sharing apps and all the other software of today.

I've worked on software for internal use in manufacturing, and number #1 problem I had was that the customer had a bunch of unclear ideas (ideas that I, a lowly developer with zero experience in the domain, had to fix for them on the whiteboard during meetings many times, because thinking clearly is not a common skill, and they did not have it). A lot of consumer-grade software try to get around this by giving up on clear thinking altogether, and just do gradient descent on customer demands (as perceived through A/B tests) in order to maximize money made, regardless of whether the product ends up being useful or not. I don't feel industrial software lends itself to such method; hell, I hope it doesn't - I'd prefer the firmware running in factories to be effective, not addictive.

You and twic make similar points, which I think are reasonable but miss a very fundamental difference between e.g., ecommerce webapps and something like a robot.

The how and what questions in robotics/manufacturing ground out in formal methods style mathematical modeling in a way that the sort of questions that dominated the last couple cycles of tech did not (because those tended to be behavioral specifications about humans -- click more ads, book more taxis, click the buy button, etc).

Formal methods didn't capture "engagement" or "click-through rate", but they do capture "safety" and "liveness".

Consider any of the examples you give. At the top level of the design process, we need to derisk things that demand mathematical modeling (battery life, car behavior). How do you go about determining the probability of a car colliding, or tease out the various things that might inform that probability? Not (only) by white boarding with business stakeholders or asking consumers, but (also) by building models of how the system behaves and analyzing those models.

Obviously, formal methods aren't a silver bullet, and yes, software engineers will always spend a lot of time at whiteboards and in meetings.

But when it comes to the future of formal methods, the question is whether the systems we expect to take center stage in the software world look like to sorts of systems where properties like "safety" and "liveness" are a) hard to specify, b) lend themselves to mathematical analysis, and c) are critical to business success.

I think the answer to that question is yes.

> automated trading

> It's really obvious what we want the system to do

Nope.

Buy low, sell high!

>> It's really obvious what we want the system to do

>Nope.

Hedge funds and trading firms are some of the top donors to/supporters of the formal methods community. They sponsor conferences, hire tons of formal methods experts, buy products and services from formal methods startups, and develop/use formal methods internally.

So...

Yup.

(I do understand there's a substantive point being made, and I think my reply to the sibling comment by temporal addresses that point. So maybe that's the right place to continue discussion.)

> The really simple answer to this question is: because at a high level of abstraction, it isn't useful.

Okay, but if you're implementing a complicated algorithm like Paxos or Draft, then it can be useful to put some assertions in your code, and prove them in a formal language; and also to make these proofs part of the unit tests.

Strong type systems are not new.

Strong type systems with type inference are new(ish) for a guy as old as me :-D

Standard ML has existed for 35 years. Even if you started programming with Fortran, it's been around longer than half of your career.

Be honest, until 10y ago, ml type inference was invisible to 90% of the coders. Probably rejected willingly even ('where are my objects?')

I learned Haskell in 2001, was super excited by it but there wasn’t the “day to day” stuff to get things done that you had in Java or C++. So for practical work I felt I couldn’t use it. Fast forward now, with the rise of open source sand devs volunteering to code in their free time, we have Haskell kind of useful. Definitely for web software and backend. Although I question desktop development in Haskell.

> Probably rejected willingly even ('where are my objects?')

Local type inference was rejected in Java in 2001 because "you need to spec your types precisely"

is it published online ?

IIRC it was common knowledge, as it was an "obvious improvement" over C-style undeclared variables. Have in mind that type inference applied only to local values, not propagated globally through the code structure as in ML.

Found it here: https://stackify.com/whats-new-in-java-10/

——— start quote ———

This feature has been a long time coming. It was suggested as far back as 2001, and was closed at that time with the following comment by Gilad Bracha:

Humans benefit from the redundancy of the type declaration in two ways. First, the redundant type serves as valuable documentation – readers do not have to search for the declaration of getMap() to find out what type it returns. Second, the redundancy allows the programmer to declare the intended type, and thereby benefit from a cross-check performed by the compiler.

——— end quote ———

Link to original RFE and quote source: https://bugs.java.com/bugdatabase/view_bug.do?bug_id=4459053

Interesting, I kinda agree about the need for redundancy at times (which is not forbidden by ML typing). But it rejected a very good idea for a decade.. A bit like lambda expressions. Damn Java

It's even older than that. The Hindley–Milner type system was first described in 1969. In other words, we've had the foundation for this kind of type inference for 50 years.

What's the deal?

Really could be new to him. It's a pretty big world out there.

Which is why I'm amazed it's actually used now outside academia. It lingered so long there, it's surprising that it made the jump.

Probably due to some alums of INRIA using their particular implementation for their own projects.

Exactly. And releasing formally incorrect apps to non-suspecting users is the best known way to bridge that gap.

Reply on news.ycombinator.com