The final proof you get from formal methods is often irrelevant in my opinion. Most of the benefit comes from architecting the system so as much as possible can be verified and forcing yourself to make intentional decisions on the edge cases. The results are for other people.
I'm not sure you want to create a record of intentional decisions if you're at Facebook though.
The trouble is the simulation tools are either proprietary and thus have only a small mind share among software developers, or academic, and either way, PLC programmers have not gone near them yet.
But a decent LLM should be able to translate the description of a plant to a TLA+ model (or Alloy, or something similar.)
> My fraternity was more tame and we used to have guys gazing each other in the main room during parties.
Joining a fraternity makes you jointly and severally liable for anything your frat brothers do. It's the very opposite of working or investing in a limited liability company. Makes sense for a fraternity to be more tame...
Which is why I am sitting right now in a meeting and the presenter is logged in from Bangalore and I don't even want to know what `TZ=Asia/Kolkata date` will tell me.
I'm often shuffled into teams where I am the only American and everyone else is Indian, working in India, and I take a small measure of pride in switching to the formal register that Indians like to use in workplace English, and using the idioms they have.
Seems to me these LLMs have a critical mass of Python training data and Rust training data, so there's no advantage for Python there.
So as the article points out, an iterative process that catches the mistakes at compile time is much more suited for an AI than one that catches them at runtime.
This is why we need Professional Engineer licenses for software.
There are times when a product design needs to be reviewed and approved by someone who cares more about his license than about his job. It doesn't happen as often with software as it does with civil engineering, but often enough that it needs to become a thing.
And what happens when the licensing board gets politically compromised? You cant fix broken incentives by papering over another layer of administration. If the underlying incentives are opposed, the administration layer will be adapted to fit.
Civil engineering licensing works because underneath it all the incentive structure is aligned with the goals of the license. Its not about imposing morals, its about ensuring that buildings and devices are constructed to not fail, and to not fail catastrophically. The motivations of the ones who hire engineers are mostly aligned, they don't want the devices to fail either, and expose them to liability.
Medical doctor licensing also works because the incentives are mostly for patients not to be dying. But in the pharmaceuticals industry the incentive structure is different, where some rate of fatality is considered an acceptable cost of doing business, we see examples of subversion.
Sure software engineering licenses could be a great addition. But alone it will fail unless the incentive structure for those employing software engineers is aligned with the licensing goals.
The firmware for a diesel engine goes into a diesel engine. The company can be required to get a PE's signify for putting the firmware in. After that, if it's copied elsewhere, that's not their problem.
You start by verifying the permissions structure for Facebook posts.
And by verifying the shortest, least complex functions in Facebook's server side code base.
reply