Hacker Newsnew | past | comments | ask | show | jobs | submit | paulajohnson's commentslogin

A formal specification language is a programming language that we don't know how to compile.

If we can use AI to automatically implement a formal spec, then that formal specification language has just become a programming language.


> A formal specification language is a programming language that we don't know how to compile.

Not really, on both counts.

Firstly they're not really programming languages in the usual sense, in that they don't describe the sequence of instructions that the computer must follow. Functional programming languages are considered 'declarative', but they're still explicit about the computational work to be done. A formal spec doesn't do this, it just expresses the intended constraints on the correspondence between input and output (very roughly speaking).

Secondly, regarding the we don't know how to compile it aspect: 'constraint programming' and SMT solvers essentially do this, although they're not a practical way to build most software.


It is more general than that: A programming language is a formal specification language that we know how to compile.

There are plenty of formal specifications that cannot be compiled, even not by an AI. If you use AI, how do you make sure that the AI compiler compiles correctly?


> A programming language is a formal specification language that we know how to compile

Plenty of real programming languages are ambiguous in ways that surely disqualify them as formal specification languages. A trivial example in C: decrementing an unsigned int variable that holds 0. The subtraction is guaranteed to wrap around, but the value you get depends on the platform, per the C standard.

> There are plenty of formal specifications that cannot be compiled, even not by an AI. If you use AI, how do you make sure that the AI compiler compiles correctly?

By proving that the code satisfies the formal spec. Getting from a formal spec to a program (in an imperative programming language, say) can be broken down into several stages of 'refinement'. A snippet from [0] :

> properties that are proved at the abstract level are maintained through refinement, hence are guaranteed to be satisfied also by later refinements.

[0] https://www.southampton.ac.uk/~tsh2n14/publications/chapters...


A formal specification language doesn't have to be deterministic.

And yes, if you can prove that the implementation is correct with respect to the formal spec, you are good, and it doesn't really matter how you got the implementation.

Refinement is one approach, personally, I just do interactive theorem proving.


Except deciding whether an implementation exists or not is itself not a tractable problem in the general case.


This reads like a case study from "The Innovator's Dilemma" by Clayton Christensen.

TL;DR: big incumbents (e.g. IBM) get out-innovated and replaced by scrappy startups even when the incumbent sees it coming and tries to react. The incumbent's business processes, sales metrics (NPII in this story), internal culture and established customer base make it impossible for an innovative product to succeed within the company.

The incumbent produces an innovative gadget. It may even be good, but its Sales Dept earn their quarterly bonus from the existing product line sold to the existing customers. They haven't got time to go chasing small orders of the new gadget from new customers who they don't have a relationship with, and the existing customers don't see the point of the new gadget. So orders for the gadget stagnate.

Across town is the small scrappy start-up making a similar gadget. It lives on those small orders and has a highly motivated sales person who chases those orders full time. So their orders grow, their product improves from the market feedback, and one day the new gadget is actually better than the incumbent's main product. At that point the incumbent goes out of business.


It actually is a case study from the Innovator's Dilemma:

    Yet IBM’s success in the first five years of the personal computing industry stands in stark contrast to
    the failure of the other leading mainframe and minicomputer makers to catch the disruptive desktop
    computing wave. How did IBM do it? It created an autonomous organization in Florida, far away from its
    New York state headquarters, that was free to procure components from any source, to sell through its own
    channels, and to forge a cost structure appropriate to the technological and competitive requirements
    of the personal computing market. The organization was free to succeed along metrics of success that were
    relevant to the personal computing market. In fact, some have argued that IBM’s subsequent decision to
    link its personal computer division much more closely to its mainstream organization was an important
    factor in IBM’s difficulties in maintaining its profitability and market share in the personal computer
    industry. It seems to be very difficult to manage the peaceful, unambiguous coexistence of two cost
    structures, and two models for how to make money, within a single company.


IBM didn't create an innovative product though. If you look at the era, there were dozens of machines of a similar style on the market, either z80 or 8080, 8088, even 8086... but they ran CP/M. PC-DOS was effectively a kind of fork / rip-off of DR's CP/M, but clean room and customized for 8086.

IBM created a rather generic machine using off the shelf components, and someone else's operating system.

Innovation factor was almost zero.

The only advantage it had was it had IBM's name on it, and IBM was still a Really Big Deal then. It brought "respectability" to a thing that before was still a weird subculture.


I don’t know, I think the concept of a BIOS with a documented API and the included minimal component set (e.g. serial port, parallel port) raised the bar on what third party software could assume existed and could be accessed over the existing 8-bit computers if the time.


The IBM PC did not include a serial or parallel port. Just a keyboard port and a cassette port (the latter of which approximately nobody used)


CP/M had a BIOS with a documented API.


> The incumbent produces an innovative gadget. It may even be good, but its Sales Dept earn their quarterly bonus from the existing product line sold to the existing customers.

In a rare feat, Apple managed to do just that with the iPhone, which ate the iPod’s lunch. This at a time when the iPod was a core product, directly responsible for their revival and success, that could have been milked for years to come.


One of Apple’s founding philosophies from Steve Jobs made this explicit:

“One of Job's business rules was to never be afraid of cannibalizing yourself. " If you don't cannibalize yourself, someone else will," he said. So even though an Iphone might cannibalize sales of an IPod, or an IPad might cannibalize sales of a laptop, that did not deter him.” — Walter Isaacson


and now we have ipad that perfectly capable of running MacOs but Apple refuse to do so.


iPads already outsell Macs. I imagine Apple is willing to accept lower margin overall for iPad hardware (vs. Mac) since it gets a cut of iPad software sales on the App Store. This is perhaps a business reason for why you want macOS on an iPad and Apple does not.

However, Jobs also believed in product differentiation and thought that having too many products in the same space was confusing. Arguably by making iPadOS more macOS-like Apple is reducing that differentiation and increasing confusion.


They also kind of did it with the Mac. For 4 years after the Mac was introduced, it was still the Apple II that was paying the bills, the Mac was flopping. It took stubborn management to keep investing in the Mac and not give up on it and try to evolve the Apple II instead (imagining a future based on the IIgs here)


Ehh, im not sure they could have milked it for very long, if the iphone didn't come out somebody else would have made the same kind of device within a year or two and made ipods obsolete shortly after. PDAs were already a thing with many models and competitors, cell phone transceivers were getting far smaller and efficient, and solid state storage was getting reasonably cheap.

The most impressive thing about the iphone I didn't think has anything to do with the technology, and everything to do with timing the release of a mobile device to hit the sweet spot between the cost of the hardware and capability of the hardware.


I think you greatly underestimate the iPhone’s original impact and the reason that other very successful companies went out of business entirely due to it. It broke new ground in more than just technology e.g. also in the relationship between the phone manufacturer and the carrier, and advantage it kept for some time and in the software developed for it e.g. a full browser versus WAP.


Where I lived in Europe, by the time the iPhone came out, a lot of people (me included) were already using Sony Ericsson Walkman phones instead for music listening


This has much the same design philosophy as the original Land Rover: tough, reliable, simple and maintainable. It was originally developed as the UK answer to the Jeep, but rapidly became the standard utility vehicle for anyone with an outdoor off road job. Especially farmers. Something like two thirds of all Land Rovers ever made are still in use.

This might well go the same way.


>This has much the same design philosophy as the original Land Rover: tough, reliable, simple and maintainable

Where do you get any of this from? Especially EVs are not something you can easily tinker with as the risk of killing yourself is pretty high. In general they are also more integrated and less maintainable and it seems unlikely that this won't be the case here. Maintainability costs money and to make a 20k car happen every cent needs to be saved.

As for reliability it is obviously one of the first things to sacrifice to make low costs happen. We have seen nothing of this car, I doubt the engineering is even far along.


Gentrification doesn't reduce segregation, it just moves the boundaries of the segregated areas.

Poor people mostly rent because they can't afford or can't get a mortgage. When an area gentrifies those people are forced out because the rents rise, and wealthy people move in. If you just look at the income distribution in the area it looks like "the population" became wealthier, but if you look at the individuals you find that the old residents have been forced out, and generally wind up poorer because of this (social networks disrupted, work further away etc).


This is the Paradox of Tolerance. If you tolerate intolerance then intolerance wins, and you don't have tolerance any more.

Intolerance isn't just "causing offence", it is the creation of an environment which is threatening. If ou get enough veiled anonymous threats against your life, health and family then you might well withdraw from public life. And then, what value does "free speech" have for you?

But, you say, you aren't talking about threats, just about "offence". But offensive speech begets threats. If Mr Rabblerouse publicly calls Jenny Good out as a dangerous degenerate, some of his followers will, quite predictably, follow his lead and start to make actual threats. Some might go further and carry out those threats. Even if they do not, Ms Good is going to have a perfectly reasonable fear that they might.

You say that Mr Rabblerouse is merely stating a legitmate opinion, that he has a right to be offensive, and that the Ms Good is equally free to say unpleasant things about him. But that is just deliberately ignoring the power inequality. Ms Good has no mob who will take the hint to hate on Mr Rabblerouse, no power to put him in fear. But he does have the power to do it to her, on a whim, answerable to nobody. And when people see that, and see how easily he can put Ms Good in fear and misery, they will think twice about their own speech.

And this is the point. Hate speech is not merely unpleasant and worthless, it actively suppresses the speech of other people. US jurisprudence makes much of "chilling effects" of government action on speech, and with good reason. But it is not just the government that can chill speech. Mr Rabblerouse can chill the speech of others against himself very effectively. So the only way to ensure freedom of speech, paradoxically, is to ban speech that incites hatred.


I think the parent comment is about the likelihood of recovering enough money to make the exercise worthwhile, rather than the propriety of getting ripped off.


Yet another reason why not to be a sharecropper.


The 10 LOC/day includes the entire project, including analysis, requirements, design, documentation (user and tech), test, management etc, in a large project. Saying (as many do) that an individual programmer has produced hundreds of LOC per day is to miss the point.

You have to start by defining your terms of reference and make sure you are comparing like with like.


If you are ever in Stockholm do go and see the Vasa. The picture does not do it justice. Seriously amazing.


The ship itself is just incredible.

They also have a large collection of artifacts that were well preserved in the cold, low-oxygen environment. The most interesting item I recall was a portion of human brain from the wreck that was preserved and somehow recovered.


Taking care of the elderly is a labour intensive business. Automation doesn't clean an old person's glasses (real life example), make their bed or cook their meals.


Automation doesn't need to do any of those things (even though it eventually could). It could simply make other industries so cheap and efficient that more labor flows into elder care.


The labor intensiveness is not binary.

Specifically, if there are socialized "assisted living" facilities, or even in-the-community caregiver visitation, then the amount of caregiving work-hours per day per elderly person is X. If the only possible arrangement is getting a live-in personal care-giver, then that figures is 2X or 3X (or some factor, I don't have the figures); and most people probably just don't get care.


increased demand will drive more automation in that sector

self driving cars may be limited but they will be a great solution for the elderly


Ultrasonic cleaners, man!


Not yet.


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: