learningstud

Vibrating.

Vibe coding will create more jobs to (1) clean up the mess or (2) spread the vibe.

Regulations are even worse. Hayek explained how regulations are the main drivers of shitty companies.

Try programming in a proof assistant to see how inseparable computation and logic are. It gets more fundamental than the Curry-Howard correspondence when homotopy type theory enters the scene.

In reality, logicians and type theorists are employed in the computer science department and rightfully so. The whole field of computer science should upgrade with such influx of talent.

Nowadays, logicians and type theorists find home in the computer science department instead of the math department. My whole point is to get rid of "computer" and "science" from "computer science."

Computer science studies and invents logic whereas the math community has departed from logic as a whole.

At the very end of the video, the speaker quipped that computer science is not just about computers and an actual science doesn't have "science" in its name. The development of programming languages, compilers, SMT/MILP solvers, type theories, and proof assistants allude to the true nature of computer science, i.e., logic and its automation. It can be argued that computer science is even more fundamental than math, e.g., recursion/complexity, intuitionism/constructivism, linear logic, homotopy type theory.

The real capitalists are the board and investors.

Exactly, like Daoism.

Coordination. However, just like Hayek explained how it's much more practical and beneficial to rely on the impersonal price system for coordination than central planning. The bigger the company, the less beneficial to have CEO coordinate the company.

Or, the accountants determined that the overall cost of voluntary exits is expected to be lower than a mass layoff. It's possible that voluntary exits make more financial sense.

True, unions, in general, hurt employees no matter how competent or incompetent said unions are. Unions are the privatization of governmental bureaucracy: more evil than "exploitative" big tech corps.

Your revelations echo with that of Seneca, "On the Shortness of Life". You take your life seriously which is an act that I immensely respect.

Yes, Google gains advantages through the Chrome browser so do we as consumers. The competition for Chrome should come from a better Browser not by being forced to sell it. DOJ is wasting time and taxes on this pointless verdict. Even more economic wastes are coming when the selling happens.

This is so stupid. When will we learn some common sense from Milton Friedman?

Don't indulge in meritocracy. It's essentially a "prize".

> If the government ever wants a third party to oversee safety of openAI

No, please don't drag the government into this. Don't call for regulation when we don't know it's implications. Once we gain enough insight, the benefits of regulations and government interventions will most likely outweigh the costs. Laissez-faire is the way to go. When can we learn from history?

The engineers most likely have looked into it. Most likely, it's the legal department and higher ups that decided to push through.

Many people are already like that most of the time.

Take the aftermath of the recent Kahramanmaras earthquake, the status quo should be improved even for well established engineering fields, and more so for the software industry.

I believe software has the potential to be an exception of "any human endeavor done at scale is going to be a complete clusterfuck of a trainwreck." In software development, there are methods to scale correctness not mistakes, but they are not as prevalently used as desired. Some practical examples being:

1. Affine types in Rust.

2. Refinement types in Ada.

3. Dependent types in Coq/Agda/Lean/Idris/ATS-lang.

4. Separation logic in Facebook Infer.

These methods systematically/automatically eradicate errors that incomprehensive/human-intensive alternatives (unit-testing, code review) can't do at scale. If our industry could adopt and improve on this, we could create truly ambitious projects with confidence, at a lower cost, and at a faster pace because 1) correctness is scaled and 2) mistakes are contained.

Could it be that formal methods are exactly the solution to "wrangling clarity into requirements from messy humans"? Business people and programmers could work closely together to incrementally build a list of formal requirements with the help of proof assistants. So that both parties can know clearly what are known to be ambiguous and what can be implemented immediately at every stage of discussion. Update the formal list of requirements whenever anyone has a breakthrough. Investigate into possible inconsistency early on with the help of proof assistants. Enforce project-wide constraints for every update to the list of requirements. Cooperate to make more and more informal stuff formal to reduce misunderstanding.

Formal methods can help with exploration and cooperation.

It's never about perfection, but lifting up the acceptable lower bound. Around 150 years ago, Joseph Lister had to go to great lengths to persuade surgeons to apply antiseptics, which seems like a no-brainer nowadays. The methods I mentioned have been well-established for decades.

GitHub issues

Rarely is software engineering as currently practiced actually "engineering" and "problem solving". We are mostly creating even more problems due to unreliable methodology forced down our throat. Hell, we can't even reliably identify bugs given extensive testing, fuzzing, and code review. Fashion trends like microservices cannot contain the impact of bugs in one service; all hell break loose. Instead, microservice practice aligns the software layout with HR layout (a la Conway) even more faithfully than monoliths did, and this outcome is the antithesis of engineering.

This is what Albert Camus described as "absurd". I suggest reading "The Myth of Sisyphus". That book will shed some light on how one should live in this funny world.

There are also numerous examples to show how many people have no understanding of what he/she is actually saying. Specifically so in programming. Code snippets created by human programmers are generally only more reliable than that created by copilot by a small margin. Human programmers rarely have deep insight into the code they write unlike mathematicians often having deep insight about their theories. The fact that programmers constantly create bugs is due to their lack of understanding of the code they wrote. The only way we can stay significantly ahead of AI code generators is to program with formal methods where deep insights are directly expressed in the code whose correctness are also guaranteed by compilers at the same time.

Or, you can have complex systems with PROOFS like CompCert and Sel4. With formal methods, you can move as fast or as slow as you like.

No, most code is really just shit. The fact that code only gets more obscure instead of more obvious is anti-intellectual. This is the complete opposite of mathematical progress. It is due to the arrogance of programmers to think that their current codebase is the best TRADEOFF anyone could have achieved. Take the newcomers' words as monition. Be completely honest about how hard it is to think straight, and adopt formal methods like Coq as done by CompCert and Sel4. There is a reason why mathematicians DEMAND proofs. It's too easy to fool yourself. Recall how "newcomers" like Hilbert in the early 20th century revamped and closed "wide gaps" in Euclid's Element which had been considered the epitome of rigor for 2200 years. Of course, people will argue that proofs take too much time, etc. Wrong! Things move so much faster when there is absolute confidence that everything is correct. As proofs are required, one is also forced to constantly simplify things. This is what refactoring is all about: simplification.

It's feasible to create no bugs with formal specification and formal verification. For example, with Lean 4, one can add a proof for each array-access-by-index that the index is within the bound of the associated array. Every aspect of the codebase can be subject to formal proofs that are verified by the compiler. See also CompCert and Sel4.