And what value has the current state of AI added to society in any meaningful way? Truly? Even as someone who understands the space very strongly, and has published several top-tier ML papers, I cannot help but to conclude the primary destination of the current tech sector and Silicon Valley is the ruthless exploitation of the rest of society.
Taking a sober look at the state of software, we observe a few things.
The services offered by modern software to users, as a whole, have remained largely the same over the past ~5 years. The state of software quality is in rapid decline, with enshittification and rent-seeking running extraordinarily rampant. Software security has been in the same disaster-state it has been for the past 20 years, where software resilience is in stagnation, governments and private institutions stockpile vulnerabilities, and security researchers and auditors can consistently find new vulnerabilities. The rest of American society outside of the tech sector is currently facing a standards of living nosedive, and clearly they have not benefited from the tech sector's financial proliferation in the AI space.
Realistically, I cannot help the feeling that we're headed towards a reality where the 4th amendment is dead, and machine learning models process everything about you to ultimately extract more from you. No privacy for you! No agency for you! Only indentured servitude, and constant fear.
I fully recognize my take is ahead of its time, but I concur that the systems-oriented point of view is our way out of this hell. Specifically, software should be conceived under the following ideals: (1) software should be as simple as possible, and provide its intended services with as little bloat as possible; (2) specifications of software should be as concise and simple as possible; (3) specifications should be should be expressive enough to capture security-relevant guarantees, e.g. cryptographic security properties; (4) proofs verifying that software satisfies its specifications should live intrinsically to the implementation, and should be as simple as possible; (5) proof-checkers should be verified. I feel the academic Formal Methods, Programming Languages, Systems, Security, and Cryptography communities, as well as the internet standardization community, are slowly converging to this ideology consensus, but I also think in other ways we are farther off than ever. With respect to these ideals, the "building" mindset that twitter has adopted is deeply toxic. And obviously Silicon Valley has their heads in the sand when it comes to this.
I do have faith the state of software (and society) will improve, but whether that future is compatible with the rent-seeking hyper-capitalist reality Silicon Valley and Wall Street have synthesized is yet to be seen.
I believe this is a fundamental misjudgement of the CS curriculums at MIT and NEU and, apologies for being blunt, probably the worst take on this thread.
The student populations at MIT and NEU, particularly in CS, are fundamentally different. The majority of undergraduates at CS MIT participate in academic research while the vast majority of CS undergraduates at NEU do not (do not let NEU's exceptionally high computer science research output [1] confuse you - the undergraduate and graduate schools are very separate). MIT educates significantly less students than NEU. MIT's algorithms class (6.046) is significantly more rigorous than NEU's equivalent (CS3000) - just compare the publicly available curriculum and problem sets [2,3]. In general, MIT's CS curriculum caters towards the third of the student body that go on to do PhDs, while NEU's CS curriculum caters towards the vast majority of students that beeline towards industry [4,5]. The institutional goals and educational values between MIT and NEU could not be more different. I know all of this to be true because I've spent a significant amount of time at both institutions.
I don't know if NEU will butcher its CS curriculum. I hope not. I guess we'll just have to see.
P.S. it's worth checking out Pyret [4], essentially a functional teaching programming language. The language is mostly written by NEU staff, so I wager NEU's future CS curriculum plans to phase out Racket in favor of Pyret.
I just want to note, there exist two main flavors of formal methods: extrinsic techniques, which are disjoint from the code itself and generally reason about the specifications of code, and intrinsic techniques, which are inline with the code itself and reason about the code more directly. Historically, intrinsic techniques (such as type systems) reason about code at a functional level, while extrinsic techniques (such as decidable model checkers like Spin/P) reason about a model of the code, ascribed to formalism like an automata. But imo we're currently in a complete golden age of formal methods research, and extrinsic techniques are falling out of flavor in comparison to intrinsic methods as pushed by type system advancements and projects like Verus [1].
I don’t see how the distinction makes any sense when the Verus project you linked requires you to write correctness specs. It sounded like intrinsic techniques were preferred because they would not require you to write and maintain a separate spec, but this is not the case.
I prefer intrinsic techniques because it prevents the model from being out of sync with the implementation.
The thing that's never made any sense to me about using a marble checker for anything but concurrency issues (which are hard enough to warrant it) is that once you've validated your model you have to go actually implement it, and that's usually the most error prone part of the process.
If the correctness spec has to be written manually but prevents you from diverging from the spec in your implementation, that's a huge step up from extrinsic model checkers.
Lamport's rationale is that after an architect designs a building, the builders may still put electrical sockets in the wrong place and make other mistakes. But that's not a reason to start construction without a plan at all.
That rationale assumes that writing software has a design stage and a build stage. It doesn't—software is the design, the building is done by the compiler or interpreter at runtime. So what's really being proposed is subdividing the design stage into a pre-design and a design.
Pre-design makes sense to me in certain limited circumstances. A limited amount of architecture planning can be valuable (though in most cases formal methods aren't useful for that), and for certain kinds of concurrent algorithms it could even be worth it to validate the design in a different language. But most of the time it's not worth doing the design twice when you can get pretty good guarantees from static analysis on the design (the code) itself.
Agreed. To stretch the analogy, if I'm just replacing a fence panel or putting up a shelf then I'm not going to get an architect to create a blueprint. I'll know if it's right from the execution.
I sometimes work in areas where the error budget is essentially zero, with an element of concurrency, and for those there is a design stage before the build stage. I could see the value of formal methods there. At least I could execute a model with a model checker, which makes it one step closer to the code than a design doc or RFC.
Full disclosure: I haven't actually used formal methods myself, I've just been interested in the idea for a while and have done some reading on it.
Taking a sober look at the state of software, we observe a few things.
The services offered by modern software to users, as a whole, have remained largely the same over the past ~5 years. The state of software quality is in rapid decline, with enshittification and rent-seeking running extraordinarily rampant. Software security has been in the same disaster-state it has been for the past 20 years, where software resilience is in stagnation, governments and private institutions stockpile vulnerabilities, and security researchers and auditors can consistently find new vulnerabilities. The rest of American society outside of the tech sector is currently facing a standards of living nosedive, and clearly they have not benefited from the tech sector's financial proliferation in the AI space.
Realistically, I cannot help the feeling that we're headed towards a reality where the 4th amendment is dead, and machine learning models process everything about you to ultimately extract more from you. No privacy for you! No agency for you! Only indentured servitude, and constant fear.
I fully recognize my take is ahead of its time, but I concur that the systems-oriented point of view is our way out of this hell. Specifically, software should be conceived under the following ideals: (1) software should be as simple as possible, and provide its intended services with as little bloat as possible; (2) specifications of software should be as concise and simple as possible; (3) specifications should be should be expressive enough to capture security-relevant guarantees, e.g. cryptographic security properties; (4) proofs verifying that software satisfies its specifications should live intrinsically to the implementation, and should be as simple as possible; (5) proof-checkers should be verified. I feel the academic Formal Methods, Programming Languages, Systems, Security, and Cryptography communities, as well as the internet standardization community, are slowly converging to this ideology consensus, but I also think in other ways we are farther off than ever. With respect to these ideals, the "building" mindset that twitter has adopted is deeply toxic. And obviously Silicon Valley has their heads in the sand when it comes to this.
I do have faith the state of software (and society) will improve, but whether that future is compatible with the rent-seeking hyper-capitalist reality Silicon Valley and Wall Street have synthesized is yet to be seen.
reply