throwaway17_17

Allegedly the pre and post conditions, in varying degrees of certainty according to the evaluation semantics selected, are propagated to the optimization passes of gcc and llvm. However, I haven’t seen any detailed blog posts or summaries of the effectiveness or reliability of this feature. Sorry it’s not a lot of info, but it was what I knew off hand based on previous reading.

I agree, the only reason LSP exists as it does is for a world running on electron based applications. Plug-ins and application extensions are not new technology and they are nearly universally more efficient in the forms designed and used prior to 2005-ish. I understand why VSCode exists and why it is used so often by developers, but it is certainly a downgrade from more language specific options that could exist.

There are some arguments that do carry water in favor of using a client/server protocol transmitting JSON, in particular, the ability for a nearly complete decoupling of analysis of code and the displaying and editing of that code. Also, LSP was (to my knowledge) the first language/platform/usecase agnostic protocol intended for use in code editors.

I get why this is where a big chunk of developers have ended up, but I do bemoan the lost potential for a language to grab mindshare and popularity on the usability and performance of its tooling and developer experience via-a-vis a custom designed and hyper specific code editor. I mean, Rust and Elm received endless praise for their error messages as a massive boon to developer experience, so it is a facet of language design and implementation that can act as great advertisement. I just hate that the prevalence of LSP at this point precludes custom editors as a first choice in the current zeitgeist.

Thank you for the link to Watts’ talk. It is a great watch and is certainly a great jumping off point for anyone writing fiction in the field.

It also could be one of the most terrifying talks I’ve ever heard, but since it is eight years old, I am going to just pretend all of the research he mentions fell through and I have nothing worry about.

This being primarily generated leads me to wonder: is there a good source, written by academics or professionals, for this information?

Although I am not interested in using LLMs for much of anything, the theory and implementation (where the implementation is not just use some prepackaged library code) in a comprehensive presentation is not something I’ve seen before.

Your comment seems to imply that async/await should be or is in some setting not just sugar for promises. But, I am under the impression the async/await is (and always has been) sugar over explicit promises. Not just in JavaScript but in C#, where the sugar originates, as well.

Is there somewhere that async/await is implemented as a different concurrency mechanism?

I know it’s a late reply, but the answer is absolutely both of us are exceptionally neurotic. But in completely different ways.

After digging through a recently passed relative’s hard drive (the computer barely functioned so I pulled it) and having to search through years of garbage that where never deleted to find the photos, Word documents, and WordPerfect documents my aunt ‘knew’ where stored there somewhere, this is not an insignificant gift to leave my family with.

If you are asking in the context of Idris 2.0 (the current version), ST is not really related.

However, if you mean ST in Idris 1.0, there is a definite correlation. The mechanism that ST used for enabling local mutations was very similar to the mechanism that the typestate pattern in Rust is using. ST was a framework for formalizing State Machines in dependent types which is the mechanism TFA is analyzing.

From a language design perspective I go back and forth on named params. I think the only conclusion I’ve reached is that I am not in favor of them being optional, but I think that is more a concern for implementation of the language and less about how it effects users.

How do you find the feature useful in this instance, I can’t quite picture how that works for typestate pattern functions.

I feel so seen right now. My partner complains about me closing apps on my phone consistently. I also have to hold myself back from defragging and continually cleaning up my storage drives.

I too am nearly certain that the positive benefits are approaching nil, but I still feel it should be helpful.

I think this is a good argument for the Ticket, however, for the case where these three functions are generically useful, not just used in this specified order, I would write a specific function, just copy-paste of the bodies capturing the required ordering as an implementation detail.

Obviously if you are operating in a wide, concurrent async system then the Ticket and separate function calls is the better mechanism for the ordering.

I know this wasn’t the crux of your post, but do you find that you primarily look at types as puzzles in a majority of your code? I have a fundamentally different view and find other perspectives interesting when thinking about language design.

As a separate point, I think this is an excellent example of making invalid states unrepresentable.

Casey Muratori talk from the Better Software Conference 2026.

Has this become a ‘smell’? I tend to start my HN comments that are going be negative with versions of this, or my habitual “Genuine question, ..”; but if this is going to flag readers’ internal LLM-detector I will have to find some other way to indicate I’m actually interested in a dialogue (versus the shit posting that a more brief reply might signal).

I was talking with a junior at the office today about LLM output and mentioned em dashes, to which responded “oh, I thought that was just where formatting for hyphens was going, I guess I learned something from the AI writing instead of the other way around” and god, his acceptance of it was just deprrsssing.