learningstud

Yes, or to settle dispute and remove doubt once and for all, i.e. the Leibniz way.

All just for Apple to sue them... A SpaceMouse is way cooler.

Too true. This is why Rudin's little book, Principles of Mathematical Analysis, normally takes a whole year to cover: one has to work through the proof line by line in order gain enough understanding to do the exercises. Programming gives you the false sense of ease with leaky "interfaces" and quantum-entangled "decoupling". LOL, one microservice in one separate git repo, and tested with mocks and Gherkin syntax BDD. Just LOL, I call this hyperreal programming. With "spec-driven" AI generated code that is reviewed and tested by AI, it is certain that "the programming did not take place". In this "brave new world", "the map has overcome the territory", and "the twelfth camel" was never returned. Programmers certainly don't need "the mythical man-ager" to go delulu and full ouroboros, i.e. "there is no big Other".

What DDoS mitigations are there besides the less affordable Akamai?

I've come to believe that democracy doesn't work because most citizens don't want to work it. Many of the legislations passed are harmful to the majority even when the intentions are good. Milton Friedman, Thomas Sowell, and Friedrich Hayek have been saying this for a century.

This was the sentiment for programmers well-versed in assembly languages (counting cycles, self-modifying code, story of Mel) when compilers came out, yet the advances in compiler technology enabled the creation of OCaml and Coq. What I think will actually happen is that a new breed of programmers with extensive mathematical background will start designing unprecedented software (or even digital circuits through high-level synthesis) that are almost correct by construction at a much faster rate with the combination of formal specification and AI coding. The field of computer aided design (CAD) will likely explode, and we will witness spaceships, nanobots, etc. being churned out at the rate of React websites. The whole computing field will become so high level that applied mathematics like optimal control, optimal transport, information geometry, etc. will become bread and butter for any programmer.

At the same time, there will be a new breed of artists that starts making games, movies, etc. with AI alone. We will witness a whole new form of artistic expression.

If developers are not using TLA+ or Lean4 etc. They are vibe coding. Nothing wrong with that. They just have to realize that they were never in control. Thinking logically is much harder than developers imagined. As Dijkstra observed, the whole field has adopted the mentra, "How to program when you cannot." I estimate that 80% of what developers do can be done once and for all for all of humanity, yet we don't learn. Be offended all you want, but I am fed up with this idiocy given all the usual rebuttals of deadlines etc.

https://news.ycombinator.com/item?id=43679634

No, formal specification helps from the get-go. You can iterate more reliably, thus faster. The successful development of mathematical theories depends on having rigorous definitions and proofs all the way from the start so that people can communicate effectively, point out caveats unambiguously, and modify the theory robustly. Without formal specs/proofs, refactoring will become too hard. It's actually a lot easier to capture the behavior of a program formally than by tests. Programmers need to gain some experience in math to see this. Listen to Hoare and Dijkstra, and start "thinking".

Major flaws in a specification for one function are usually quickly picked up when the proof for another function relies on the missing specification properties

Great point! In a sense, it's testing by immediate use at compile time. I always imagine this to be the greatest productivity booster, even greater than AI. You'll notice things are wrong as you type.

Yeah, that's why I mentioned Lean 4, Agda, and Rocq. Homotopy type theory is even better; see it's definition of a circle.

Architecture astronaut type of stuff indicates programmers' lack of critical thinking. People are just hopelessly dim.

Naive optimism, sheer ignorance, and a general inability to think.

Let's face it. Can you claim that the code you wrote yesterday is free of errors? Most programmers cannot, yet everyone that studied calculus knows that the fundamental theorem of calculus is true without the need to test it again and again because mathematicians proved it. As if the development of logic in the 20th century was nothing, programmers keep thinking that logic is an innate skill that doesn't require focused study. The fact that programs become more incomprehensible instead of gaining more clarity as in math points to the anti-intellectual tendency of programmers and their general inability to think. Programmers have been vibe coding long before the introduction of AI agents.

LLM or not, most programmers cannot think straight. LLMs just lead to more false impressions of understanding. When LLMs become really good, they will refuse doing your work for you out of distaste.

This speaks volumes of why the Elixir people left in the first place.

As a separate point, if a company wants the most generally applicable programming language, there is no reason to look further than C, yet few companies are like this.

The OCaml people probably know C/C++ better than most C/C++ programmers. Do you even know any of them?

Lesser pay is simply due to less demand. It simply reflects the overall needs of living people.

I really don't get why people would want AI to think like humans even remotely, especially when we don't even know how humans think. Most people simply cannot provide justification for whatever comes out of their mouths, e.g. try explaining how planimeters work for contours that are not differentiable at every point. This question will bring out the LLM-like behavior in people.

Edsgar Dijkstra!

Exactly, most of us behave in almost the same as AI does. We finally have a mirror to reflect upon.

Validity is not soundness. Wonder why people are just beginning to realize what logicians have been studying for more than a century. This goes to show that most programming was never based on logic but vibes. People have been vibe coding with themselves before AI became prominent.

People hallucinate all the time out of pressure or habit. We don't need AI for that. It's hard to tell most people from AI. Most people would fail Turing tests as subjects.

To say the least, requiring FDA to approve drugs and medical doctors get licenses actually harm citizens. These claims might seem absurd at first glance, but please give Hayek's book "The Road to Serfdom" a read before contending. Hayek changed my whole life.

Wittgenstein would be flabbergasted by the misguidedness of vibe coding.

For UML to capture the logic of the programs it describes, UML will have to become a feature-rich programming language itself. Then, we will witness how unreadable a bunch of arrows are compared to well-structured texts. Semantics is essential complexity that stays the same whereas UML has more accidental complexity than, say, the C language.

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."