For what it’s worth, Claude did this without even being asked when I had it implement /dev/urandom in my deterministic dotnet runtime. (Fun fact: if the runtime only ever receives zero bytes from /dev/urandom then it will hang on attempting to initialise System.Random! That was the first way I asked for it to be implemented.)
Does it have a terse syntax? I main F#, and when I have to work with Python I generally find myself complaining about how verbose it is. (Needing intermediate variables for what should have been a pipeline, the ceremony around parallelism, having to store constructor parameters as object fields, etc.)
It sure does in comparison with most mainstream statically typed languages — if you feel that way about Python, I wonder what you say about Java, C++ or even Rust or Go?
Checking some examples at https://learn.microsoft.com/en-us/dotnet/fsharp/tour, I'd say it's quite similar in verbosity — eg. no need to declare a module in Python since the code already lives in a file that is the module (plus one less indentation level for module level functions); inline function declaration and calling is thereabouts with F# slightly more terse (let vs lambda + spaces vs parenthesis); if-then more verbose in F# (no then in Python, just "if x:"); F# does not seem to need "return"...
In many cases you can avoid intermediate varibles: inline ifs, list comprehensions, lambdas, etc... Constructor arguments are a good point, but this is mostly about idiomatic use instead of language itself: you can simply do
def __init__(self, **kwargs):
self.args = kwargs
I'll give you one on the ceremony around concurrency, though! I have different ideas of how it should have been done to shift the cost to the language runtime instead of the developer, but alas... :)
I didn't want to reimplement all the assembly-reading nonsense that comes for free with System.Reflection.Metadata. The `dotnetdll` crate exists but is GPL. Also in F# I can fall back to the CLR for fiddly things I don't want to implement (like the arithmetic opcodes on floats or whatever).
I mean, there is a reason the MIT licence contains these words:
> THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND… INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF… FITNESS FOR A PARTICULAR PURPOSE…
If you would like a tool built with my organic artisanal human fingers, then I am certainly open to sufficiently large offers of money to build one for you! Alternatively, you can simply not use it if you think it won't fit your needs :)
I think the Stroop effect ("read these colour names, each written in a different colour") is probably the purest demonstration of this. Humans are trivially prompt-injectable.
To answer your question, although I would certainly have preferred you to phrase your comments less insultingly: this project would otherwise never have got to a state where it could find bugs. I am not paid to write this code, and it would have taken far more years than I would have been willing to spend.
It's not actually unheard of for people to pay other entities to build their passion projects. For example, I visited [Eltham Palace](https://en.wikipedia.org/wiki/Eltham_Palace) last weekend, which was not in fact built entirely by the two Courthaulds who commissioned it.
Don't feel bad, there's a lot of blind hatred. I too build some things I architected similarly, things that I know take companies many a buck and years to build.
What does that have to do with LLMs? There's morev to delivering value to the customer than just shipping code. We used to understand that technical debt was an existential risk to a project. I can't see how "code nobody understands" is not technical debt.
I disagree. Shipping functionality that works and users consume is all that matters. Everything else is noise. Technical debt can be viewed through this lens - it reduces the rate in which functioning code is shipped. That's bad, but it's only one of many dials.
The author states they feel that using LLMs allowed them to ship years faster. That's years of time in which they can collect feedback and iterate. They might even choose to scrap the entire project and rewrite it based on their learnings. The practicality of this is directly enabled by agentic coding.
Technical debt is aptly named. From time to time it demands it's interest in the form of delaying a new feature, but as long as your overall technical revenue is positive, it's fine.
It sort of isn’t though, because it gives the wrong impression to people who look at things through a financial lens.
There’s no accrued compound interest: if you leave a piece of “indebted” software alone, you don’t pay any “interest”.
Conversely, a small amount of tech debt can actually cost huge amount… but only if you make many changes at a high rate.
That’s why I prefer the “worn tools” or “sand in the gears” analogies because they provide the right financial mental model.
An unlubricated, worn out piece of industrial machinery costs you nothing… unless you try to make things with it.
You can take this analogy quite far: sharp and lubricated but outdated machinery may work “just fine”, but you won’t be able to attract the top talent used to working with modern 5-axis CnC tools instead of having to manually turn cranks like a savage.
They say in the Lean Zulip thread that this is actually intentionally a "low quality" release (https://leanprover.zulipchat.com/#narrow/channel/583336-Auto...); the paper notes that the quality is "inferior to that of expert-written Lean code". Then again, "Our results suggest that formalizing the core textbook infrastructure of modern mathematics is within reach".
I'm not, but is it yet possible to use the Vision Pro as a window manager for macOS? I'd totally get one if it were possible to lay out ordinary macOS windows in space rather than being confined to the simulation of a single rectangular screen.
I think the Steam Frame must support this once it comes out. Either first-party, or third-party. We've never had a trivially hackable, full-Linux HMD before. With known hardware like the Frame's, it should be incredibly possible to develop a VR-native Wayland compositor
On macOS, it is ultimately the app developer who is responsible for persisting and using state for windows, such as size and position. Think several terminal sessions - the terminal app needs to be the one to determine if it is representing the same 'session' as before after a restart.
If you are talking about remote display in a 3D space, the application would need to understand how to track and reopen a window in a particular location, and also there would need to be policy on how say a resize on the Vision Pro relates to the native window size once the Vision Pro is turned off.
This puts a lot of responsibility in the app developer's hands, where it is most likely not going to be accepted. So I would expect the experience to be sub-par.
There could be interesting workarounds for full-screen windows, since there are already the concepts of multiple heterogenous displays and display resolution changes on macOS. So you might have a screen, but the 'full screen' button is replaced by one which breaks the window out. The challenge would be making these persistent across connections to the Mac in a way that apps work well by default without picking up odd heuristics.
Yeah this seems like an obvious thing that would make it a lot more useful. Sad that Apple is barely scratching the surface of what’s possible, and it’s too closed for third-party developers to attempt to do anything like that.
At least for now, no, it is not possible. I agree that what you describe is how it ought to work in an ideal world, but it would probably require some serious rethinking of macOS UI/UX in order to make it work. For instance, it is not obvious what’s the best way to transfer the dock and the menu bar to a screen-less environment.
A hybrid solution I would love to see would be to have the current virtual screen, but with the option of dragging individual windows out of the screen.
reply