The issue is that it might look good but an LLM often inserts weird mistakes.
Or ellipses.
Or overindex on the training data.
If someone is not careful it is easy to completely wreck the codebase by piling on seemingly innocuous commits.
So far I have developed a good sense for when I need to push the llm to avoid sloppy code. It is all in the details.
But a junior engineer would never find/anticipate those issues.
I am a bit concerned. Because the kind of software I am making, a llm would never prompt on its own.
A junior cannot make it, it requires research and programming experience that they do not have.
But I know that if I were a junior today, I would probably try to use llms as much as possible and would probably know less programming over time.
So it seems to me that we are likely to have worse software over time.
Perhaps a boon for senior engineers but how do we train junior devs in that environment? Force them to build slowly, without llms? Is it aligned with business incentives?
Do we create APIs expecting the code to be generated by LLMs or written by hand?
Because the impact of verbosity is not necessarily the same.
LLMs don't get tired as fast as humans.
> So it seems to me that we are likely to have worse software over time.
IMO, it's already happening. I had to change some personal information on a bunch of online services recently, and two out of seven of them were down. One of them is still down, a week later. This is the website of a major utilities company. When I call them, they acknowledge that it's down, but say my timing is just bad. That combined with all the recent outages has left me with the impression that software has been getting (even more) unreliable, recently.
They are trained on code people had to make sacrifices for: deadlines, shortcuts, etc. And code people were simply too ignorant to be writing in the first place. Lots of code with hardly any coding standards.
So of course it’s going to generate code that has non-obvious bugs in it.
Ever play the Undefined Behaviour Game? Humans are bad at being compilers and catching mistakes.
I’d hoped… maybe still do, that the future of programming isn’t a shrug and, “good enough.” I hope we’ll keep developing languages and tools that let us better specify programs and optimize them.
You can also run a Forgejo instance (the software that powers Codeberg) locally - it is just a single binary that takes a minute to setup - and setup a local mirror of your Codeberg repo with code, issues, etc so you have access to your issues, wiki, etc until Codeberg is up and Forgejo (though you'll have to update them manually later).
I hope Codeberg is able to scale up to this surge in interest, but
> it is just a single binary that takes a minute to setup - and setup a local mirror of your Codeberg repo with code, issues, etc so you have access to your issues, wiki, etc
is really cool! Having a local mirror also presumably gives you the means to build tools on top, to group and navigate and view them as best works for you, which could make that side of the process so much easier.
> you'll have to update them manually later
What does the manually part mean here? Just that you'll have to remember to do a `forgejo fetch` (or whatever equivalent) to sync it up?
Human intelligence is emergent from physical/material interactions. It is constant and self-evolutive.
Artificial intelligence is data processing of a very limited number of inputs, ignoring all others. Less likely to become self-conscious. This is for now just a super calculator/ prediction machine. And it is probably better that way.
The "thinking" processi didn't evolve from silicium interacting with oxygen.
The gradient is not over physical data but purely digital information.
In a nutshell, we have the body before the brain, while AIs have the brain before the body.
I've heard it defined as the ability to learn quickly. Not just in the narrow, academic sense, but also by observing the world and people and drawing conclusions about them. It has to do with pattern recognition and abstraction.
Usually these people are knowledgeable because they are constantly learning. Eventually they become wise.
But if you compare google trends you will find that the crossover point of react vs jQuery was somewhere around 2018.
In other terms, jQuery usage was much more widespread but it is not used for new projects anymore.
The trends of Google search doesn't imply anything by itself, just that less people search Google for jQuery than React. Which isn't entirely surprising in my view - people use search engines to learn about something they're unfamiliar with. That doesn't necessarily correlate with increased usage. I've searched for React (although not on Google) but never used it.
It wouldn't be too much work to understand a bit more about the comparative usage. Looking at recent commits of projects on GitHub would be a good start, but also skewed towards open source projects which doesn't represent all actual usage of course.
Another way would be to look through historic changes to websites to see if there's any changes to the source. It'd be a bit complicated because content changes don't necessarily mean anyone is touching jQuery or React pieces.
This also ignores any sort of private usage, which you won't get any reliable data on, and may represent a significant amount of actual usage.
At the end of the day, there's only so much accurate data available to make accurate conclusions about usage of software libraries that don't phone home. The best data available, as far as I'm concerned, is what I posted earlier - and it's still not perfect and doesn't support any claims other than what the data shows.
As a side note, I don't have any dog in this race. I do think it's interesting to get a better understanding of what pieces of software are being used, by whom, in what amount, etc. but it's difficult.
No, you see the trends. You see that people have been looking less and less for jQuery and more and more for React.
But React hasn't reached the height of jQuery at its peak.
I would not be surprised if you're right in your assertion of what's used more for new projects. I still don't think the evidence you provided is enough to be so certain.
If I want to look up documentation for jQuery, I don't google the term "jquery" to find their docs. I just go straight to the docs directly. For a lot of situations, people's IDEs do enough work to not google something.
But that wouldn't still explain why searches for the term has decreased.
Besides, people in general do look up to the online documentation or links to the documentation from stack overflow.
Used to be a Google X. Not sure at what scale it was.
But if any state/central bank was clever they would subsidize this.
That's a better trickle down strategy.
Until we get to agi and all new discoveries are autonomously led by AI that is :p
> Google X is a complete failure
- Google Brain
- Google Watch/Wear OS
- Gcam/Pixel Camera
- Insight (indoor GMaps)
- Waymo
- Verily
It is a moonshot factory after all, not a "we're only going to do things that are likely to succeed" factory. It's an internal startup space, which comes with high failure rates. But these successes seem pretty successful. Even the failed Google Glass seems to have led to learning, though they probably should have kept the team going considering the success of Meta Raybands and with things like Snap's glasses.
Didn't the current LLMs stem from this...? Or it might be Google Brain instead. For Google X, there is Waymo? I know a lot of stuff didn't pan out. This is expected. These were 'moonshots'.
But the principle is there. I think that when a company sits on a load of cash, that's what they should do. Either that or become a kind of alternative investments allocator. These are risky bets. But they should be incentivized to take those risks. From a fiscal policy standpoint for instance.
Well it probably is the case already via lower taxation of capital gains and so on.
But there should probably exist a more streamlined framework to make sure incentives are aligned.
And/or assigned government projects?
Besides implementing their Cloud infrastructure that is...
I am slowly trying to understand dependent types but the explanation is a bit confusing to me as, I understand the mathematical terminology of a function that may return a type, but...
Since function types take a value and return a value, they are by definition in another universe from say morphisms that would take a type and return a type.
The same way, I see a value as a ur-element and types as sets of values.
So even if there is syntactic sugar around the value <-> type equivalence, I'd naively think that we could instead define some type morphism and that might be more accurate. The value parameter would merely be declared through a type parameter constrained to be a singleton.
The same way a ur-element is not a set but a member of set.
Then the question is representation but that could be left as an optimization.
Perhaps that it is already what is done.
Example:
type Nine int = {9}
And then the rest is generic functions, parameterizable by 9, or actually, Nine.
So nothing too different from a refinement of int.
Basically, 'value' would be a special constraint on a type parameter in normal parametric polymorphism implementations. There would probably be derived constraint information such as size etc...
But I guess, the same issue of "which refinement types can be defined, while keeping everything decidable" remains as an issue.
Also how to handle runtime values? That will require type assertions, just like union types?
Or is it only a compile time concept and there is no runtime instantiations.
Only some kind of const generics?
A typeof function could be an example of dependent type though? Even at runtime?
In the style of the linked post, you'd probably define a generic type (well, one of two generic types):
type ExactlyStatic : (0 t: Type) -> (0 v: t) -> Type
type ExactlyRuntime : (0 t: Type) -> (v: t) -> Type
Then you could have the type (ExactlyStatic Int 9) or the type (ExactlyRuntime Int 9).
The difference is that ExactlyStatic Int 9 doesn't expose the value 9 to the runtime, so it would be fully erased, while (ExactlyRuntime Int 9) does.
This means that the runtime representation of the first would be (), and the second would be Int.
> Also how to handle runtime values? That will require type assertions, just like union types?
The compiler doesn't insert any kind of runtime checks that you aren't writing in your code. The difference is that now when you write e.g. `if condition(x) then ABC else DEF` inside of the two expressions, you can obtain a proof that condition(x) is true/false, and propagate this.
Value representations will typically be algebraic-data-type flavored (so, often a tagged union) but you can use erasure to get more efficient representations if needed.
In type theory, all singleton types are isomorphic and have no useful distinguishing characteristics (indeed, this is true of all types of the same cardinality – and even then, comparing cardinalities is always undecidable and thus irrelevant at runtime). So your Nine type doesn’t really make sense, because you may as well just write Unit. In general, there is no amount of introspection into the “internal structure” of a type offered; even though parametricity does not hold in general (unless you postulate anticlassical axioms), all your functions that can run at runtime are required to be parametric.
Being isomorphic is not the same as being identical, or substitutable for one another. Type theory generally distinguishes between isomorphism and definitional equality and only the latter allows literal substitution. So a Nine type with a single constructor is indeed isomorphic to Unit but it's not the same type, it carries different syntactic and semantic meaning and the type system preserves that.
Some other false claims are that type theory does not distinguish types of the same cardinality. Type theory is usually intensional not extensional so two types with the same number of inhabitants can have wildly different structures and this structure can be used in pattern matching and type inference. Cardinality is a set-theoretic notion but most type theories are constructive and syntactic, not purely set-theoretic.
Also parametricity is a property of polymorphic functions, not of all functions in general. It's true that polymorphic code can't depend on the specific structure of its type argument but most type theories don't enforce full parametricity at runtime. Many practical type systems (like Haskell with type classes) break it with ad-hoc polymorphism or runtime types.
This comment contains a lot of false information. I’m first going to point out that there is a model of Lean’s type theory called the cardinality model, in which all types of equal cardinality are modelled as the same set. This is why I say the types have no useful distinguishing characteristics: it is consistent to add the axiom `Nine = Unit` to the type theory. For the same reason, it is consistent to add `ℕ = ℤ` as an axiom.
> So a Nine type with a single constructor is indeed isomorphic to Unit but it's not the same type, it carries different syntactic and semantic meaning and the type system preserves that.
It carries different syntax but the semantics are the exact same.
> Type theory is usually intensional not extensional so two types with the same number of inhabitants can have wildly different structures
It is true that type theory is usually intensional. It is also true that two types equal in cardinality can be constructed in multiple different ways, but this has nothing to do with intensionality verses extensionality – I wouldn’t even know how to explain why because it is just a category error – and furthermore just because they are constructed differently does not mean the types are actually different (because of the cardinality model).
> Cardinality is a set-theoretic notion but most type theories are constructive and syntactic, not purely set-theoretic.
I don’t know what you mean by this. Set theory can be constructive just as well as type theory can, and cardinality is a fully constructive notion. Set theory doesn’t have syntax per se but that’s just because the syntax is part of logic, which set theory is built on.
> most type theories don't enforce full parametricity at runtime
What is “most”? As far as I know Lean does, Coq does, and Agda does. So what else is there? Haskell isn’t a dependent type theory, so it’s irrelevant here.
---
Geniune question: Where are you sourcing your information from about type theory? Is it coming from an LLM or similar? Because I have not seen this much confusion and word salad condensed into a single comment before.
I will let Maxatar responds if he wants to but I will note that his response makes much more sense to me than yours as someone who uses traditional programming language and used to do a little math a couple decades ago.
With yours, it seems that we could even equate string to int.
How can a subtype of the integer type, defined extensionally, be equal to Unit? That really doesn't make any sense to me.
> it is consistent to add `ℕ = ℤ` as an axiom
Do you have a link to this? I am unaware of this. Not saying you're wrong but I would like to explore this. Seems very strange to me.
As he explained, an isomorphism does not mean equality for all I know. cf. Cantor. How would anything typecheck otherwise? In denotational semantics, this is not how it works.
You could look into semantic subtyping with set theoretic types for instance.
type Nine int = {9} defines a subtype of int called Nine that refers to the value 9.
All variables declared of that type are initialized as containing int(9). They are equal to Nine.
If you erased everything and replaced by Unit {} it would not work. This is a whole other type/value.
How would one be able to implement runtime reflection then?
I do understand that his response to you was a bit abrupt. Not sure he was factually wrong about the technical side though. Your knee-jerk response makes sense even if it is too bad it risks making the conversation less interesting.
Usually types are defined intensionally, e.g. by name. Not by listing a set of members (extensional encoding) in their set-theoretic semantic. So maybe you have not encountered such treatment in the languages you are used to?
edit: the only way I can understand your answer is if you are only considering the Universe of types as a standalone from the Universe of values. In that universe, we only deal with types and types structured as composites in what you are familiar of perhaps?
Maybe then it is just that this Universe as formalized is insufficiently constrained/ underspecified/ over-abstracted?
It shouldn't be too difficult to define specific extensional types on top, of which singleton types would not have their extensional definitions erased.
> Many practical type systems (like Haskell with type classes) break it with ad-hoc polymorphism or runtime types.
Haskell does not break parametricity. Any presence of ad-hoc polymorphism (via type classes) or runtime types (via something like Typeable, itself a type class) is reflected in the type signature and thus completely preserves parametricity.
How does it become Unit if it is an integer of value 9?
Why would cardinalities be undecidable if they are encoded discretely in the type?
For instance, type Nine int = {9} would not be represented as 9. It would probably be a fat pointer.
It is not just an int, it would not even have the same operations (9 + 9 is 18 which is an int but is not of type Nine, but that's fine, a fat pointer does not need to share the same set of operations as the value it wraps).
It could be seen as a refinement of int?
I am not sure that it can truly be isomorphic? My suspicion was that it would only be somewhat isomorphic at compile time, for type checking, and if there is a mechanism for auto unwrapping of the value?
There's only one possible value of type Nine; there's only one possible value of type Unit. They're isomorphic: there's a pair of functions to convert from Nine to Unit and from Unit to Nine whose compositions are identities. Both functions are just constants that discard their argument un-inspected. "nineToUnit _ = unit" and "unitToNine _ = {9}".
You've made up your language and syntax for "type Nine int = {9}" so the rules of how it works are up to you. You're sort of talking about it like it's a refinement type, which is a type plus a predicate over values of the type. Refinement types aren't quite dependent types: they're sort of like a dependent pair where the second term is of kind Proposition, not Type; your type in Liquid Haskell would look something like 'type Nine = Int<\n -> n == 9>'.
Your type Nine carries no information, so the most reasonable runtime representation is no representation at all. Any use of the Nine boils down to pattern matching on it, and a pattern match on a Nine only has one possible branch, so you can ignore the Nine term altogether.
It is an integer. It is in the definition.
And any value should be equal to nine.
By construction Nine could have been given the same representation as int, at first. Except this is not enough to express the refinement/proposition.
One could represent it as a fat pointer with a space allocated to the set of propositions/predicates to check the value of.
That allows to check for equality for instance.
That information would not be discarded.
This is basically a subtype of int.
As such, it is both a dependent type and a refinement type. While it is true that not all refinement types are dependent types, because of cardinality.
I think Maxatar response in the same thread puts it in words that are possibly closer to the art.
The predicate gets tested every time we do type checking? It is part of the type identity.
And it is a dependent type. Just like an array type is a dependent type, the actual array type depending on the length value argument.
edit: I think I am starting to understand. In the implementations that are currently existing, Singleton types may be abstracted. My point is exactly to unabstract them so that the value is part of their identity.
And only then we can deal with only types i.e. everything from the same Universe.
> The predicate gets tested every time we do type checking? It is part of the type identity.
When does type checking happen?
I think it happens at compile time, which means the predicate is not used for anything at all at run time.
> edit: I think I am starting to understand. In the implementations that are currently existing, Singleton types may be abstracted. My point is exactly to unabstract them so that the value is part of their identity.
I am not sure what you mean by "to unabstract them so that the value is part of their identity", sorry. Could you please explain it for me?
> And only then we can deal with only types i.e. everything from the same Universe.
If you mean avoiding the hierarchy of universes that many dependently typed languages have, the reason they have those is that treating all types as being in the same universe leads to a paradox ("the type of all types" contains itself and that gets weird - not impossible, just weird).
> the predicate is not used for anything at all at run time.
It is used for its value when declaring a new variable of a given type at runtime too. It has to be treated as a special predicate.
The allocator needs to be aware of this. Runtume introspection needs to be aware of this.
Parametric type instantiation also needs to know of this since it is used to create dependent types.
The point is that in the universe of types that seems to be built in dependent types, singleton Types are just Types decorrelated from their set of values. So they become indistinguishable from each other, besides their name. Or so it seems that the explanation is. It is abstracted from their value.
The proposal was to keep the set definition attached. What I call unabstract them.
The point is exactly to avoid mixing up universes which can lead to paradoxes. Instead of dealing with types as some sorts of values with functions over types, mixed up with functions over values which are also types and then functions of types and values to make some sort of dependent types, we keep the algebra of types about types.
We just bridge values into singleton types.
Also, it should allow an implementation that relies mostly on normal constrained parametricity and those singleton types.
The point is that mixing values and types (as values) would exactly lead to this type of all types issue.
But again, I am not familiar enough with the dependent type implementations to know exactly what treatment they have of the issue.
Hi aatd86! We had a different thread about existence a couple days ago, and I'm just curious -- is English your second language? What's your first language? I'm guessing French, or something from Central Europe.
Functions that return types are indeed at a higher level than those that don't.
Values can be seen as Singleton types. The key difference is the universe they live in. In the universe of types, the level one level below is perceived as a value. Similarly, in the universe of kinds, types appear to be values.
> Basically, 'value' would be a special constraint on a type parameter in normal parametric polymorphism implementations
Yes this is a level constraint.
> But I guess, the same issue of "which refinement types can be defined, while keeping everything decidable" remains as an issue.
If you're dealing with fully computable types. Nothing is decidable.
> Also how to handle runtime values? That will require type assertions, just like union types? Or is it only a compile time concept and there is no runtime instantiations. Only some kind of const generics?
A compiler with dependent types is essentially producing programs that are itself embedded with its input. There cannot be a distinction between runtime and compel time. Because in general type checking requires you to be able to run a program. The compilation essentially becomes deciding which parts you want to evaluate and which parts you want to defer until later.
> A typeof function could be an example of dependent type though? Even at runtime?
Typeof is just const.
Typeof: (T : type) -> (x:T) -> Type
Final note: I've written some compilers for toy dependently typed languages. By far dependent typing makes both the language and the compiler easier not harder. This is because Haskell and c++ and other languages with type systems and metaprogramming or generics actually have several languages: the value language that we are familiar with, but also the type language.
In Haskell, this is the class/instance language which is another logic programming language atop the lambda calculus language. This means to write a Haskell compiler you have to write a compiler for Haskell and the logic programming language (which is turing complete btw) that is the type language
Similarly in c++, you have to implement c++ AND the template system which is a functional programming language with incredibly confusing semantics.
On the other hand for a dependently typed language, you just write one language... The types are talked about in the same way as values. The only difficulty is type inference. However, an explicit dependently typed language is actually the easiest typed compiler to write because it's literally just checking for term equality which is very easy! On the other hand with a dependent language, type inference is never going to be perfect so you're a lot freer to make your own heuristic decisions and forego HM-like perfection.
But a junior engineer would never find/anticipate those issues.
I am a bit concerned. Because the kind of software I am making, a llm would never prompt on its own. A junior cannot make it, it requires research and programming experience that they do not have. But I know that if I were a junior today, I would probably try to use llms as much as possible and would probably know less programming over time.
So it seems to me that we are likely to have worse software over time. Perhaps a boon for senior engineers but how do we train junior devs in that environment? Force them to build slowly, without llms? Is it aligned with business incentives?
Do we create APIs expecting the code to be generated by LLMs or written by hand? Because the impact of verbosity is not necessarily the same. LLMs don't get tired as fast as humans.
reply