mFixman

I saw this talk in person, and I liked so much it inspired to spend four years doing a PhD in automated theorem proving.

As things stand, I'm starting one this October!

Would this mean that the trading hours for stock of companies listed in both NYSE branches would be extended by one hour due to time differences?

I can't believe Microsoft finally made Windows open source.

That's a good reason to include the tax in the price in the US. How would consumers know how much they will pay otherwise?

"M"?

> I was a L5 IC at the time

Kudos to Google for hiring extremely competent people, but I'm surprised that the creator and main architect of Keras hadn't been promoted to Staff Engineer at minimum.

I have four different apps on my phone all called "Messenger".

There must something about companies wanting their customers think that they don't need to use the competition.

"Prove that you voted for Putin or you are out of a job".

Also, if you prefer using AI assistants as desktop apps that feel separate to the browser and you can open directly, you can download Progressive Web Apps for Firefox [1] and create a separate shortcut for a sandboxed profile of Firefox with less visual clutter that open the assistant directly.

[1] https://addons.mozilla.org/en-GB/firefox/addon/pwas-for-fire...

Ironically, ChatGPT and similar LLM chatbots are great for those kinds of searches.

Being the only true 2-dimensional language, Befunge only needs the square root of the lines of code to build an equivalent program to puny 1-dimensional programs like Brainfuck or C++.

Stop trying to hire 10X engineers. Befunge applications are built by true X² engineers.

> As a user, I don’t really care.

People should understand and be able to tinker with the tools they use.

The tragedy of personal computing is that everything is so abstracted away that users use only a fraction of the power of their computer. People who grew up with modern PCs don't understand the concept of memory, and younger people who grew up with cellphones don't understand the concept of files and directories.

Open-weight AI models are great because they let normal users learn how they can make the model work for their particular use cases.

Should HN have addiction warning labels?

These MBA-approved use cases for AI feel like the Futurama parody of The Twilight Zone.

The one from Google the AI a man was using to raise his child convinced him to use Gemini to write an admiration letter to an athlete wouldn't look out of place in the series.

> If public were the default, you'd end up having to make other functions `priv fn` instead.

My guilty pleasure is Go's visibility system, where all functions that start with lowercase are private to the scope of the current class/file and all Functions that start with Uppercase are public.

It doesn't look but it would work and it's a mess when you need acronyms, but it somehow works great and the result looks nice.

I thought the opposite: if CUDA were easy to replace, wouldn't it have been replaced already?

PyTorch supports both ROCm and Ibex, but it's support is spotty and incomplete to the point where it becomes a pain to use despite AMD spending billions on improving its software layer.

NVIDIA is reaping a decade of design decisions on CUDA compatibility made less sloppily than its competitors.

They could at least use a Wacom.

This is fantastic!

I wish there was a mode where you minimise the keypresses rather than the speed; that way the best solution is Vim golfing rather than fast hjkl'ing.

Quick bug report: the character '`' appears as "Unsupported" in the leaderboard. This is very visible when following Duff's device using marks.

It would be nice to be able to toggle off `:relativenumber`.

Half the Vim users navigate large spaces by doing `42j`; have some thought for the other half that does `142G` :-)

I completely agree that trying to get an education/certification model with no feedback and simple, robotic questions is completely useless.

What's even worse is that almost none of the MOOCs used the strengths from online classes. There are other ways to learn than a hour-long video of a person talking to a webcam.

It's funny how a big part of Andrew Ng's classes is waiting for him to write text with mouse as if he were using the world's worst whiteboard; he could have prepared properly-drawn figures in advance.

> I believe this trend is a result of management culture and performance metrics that attempt to measure "impact", and correlate pay and promotions along those measures.

Meta's performance reviews are also heavily weighted for measurable impact.

I think that the reason why it's beating Alphabet in so many fronts is team culture. Most new product teams are small and have a reasonably flat hierarchy. It's easy to make impact that's both effective and measurable, and the amount of engineering time working in "useless work" is minimised.

Samsung phones have this, and I use this to play music at a pleasant low volume while watching YouTube videos at a higher volume.

I'm surprised Pixels don't; small things like this area each QoL wins.

My conspiracy theory is that renaming all products to generic names (Hangouts to Google Chat, G Suite to Google Workspace) are an attempt by Google to prevent regulators from splitting them out from the main company.

It's only a matter of time until Pixel gets renamed to "Google Phone".

Does anybody know if there's an Organic Maps equivalent for cycling?

OSM has a lot of data that's only available in everything-maps like OsmAnd, such as location of bicycle parking spaces or quality of cycle lanes. It would be nice to have it in a nicer interface than that app.

I'm currently building a bike + public transit directions engine (bringing your bike on the train). I'm surprised that this doesn't exist yet; it's my favourite way to get around!

The program seems to assume you'll clone it in your home directory, and has paths hardcoded to `~/.ellrc.d/`.

This is just bad.

And the Circle and other cut-and-cover lines.

Nevermind, I wrote that comment before my morning coffee hit.

Even if you count Euston+KX+SP as a single station, it's not that much busier in trips HS2 users from Birmingham might want to make since most trains have that as a terminus going north.

Realistically, you would only be adding access to the Thameslink and to the Northern and Victoria lines.

Old Oak Common has access to the Elizabeth Line, the two branches of the North London Line Overground, and a branch of the Lionesses Line Overground. IMO increasing Overground speed and throughput might be a better use of money than the branch line to Euston.

I wonder how the motor detection deals with groupsets with electronic shifting like Di2, which I assume are allowed in the competitions.

I'm glad that Amazon thought they could make money with Alexa; mine is currently fantastic as an universal remote control (using Zigbee) and music player (using Spotify).

I could see Ameca only being compatible with Amazon services if it had been launched a few years later.

> I think it's not correct to say that void is a monotype in C++, because the compiler won't allow you to assign the result of a function marked void to a variable, and you cannot declare a variable of type void.

The compiler does not allow you to do that particular operation out of an arbitrary restriction, but that does not make `void` a true void type. It still holds a monotype value!

  int bar() {
      std::cout << "Bar" << std::endl;
      return 0;
  }
  
  void baz() {
      std::cout << "Baz" << std::endl;
  }
  
  template <typename T> T foo(T (*f)()) {
      std::cout << "Foo" << std::endl;
      return f();
  }
  
  template <typename T> T varfoo(T (*f)()) {
      std::cout << "Varfoo" << std::endl;
      T a = f();
      return a;
  }
  
  int main()
  {
      foo(bar); // Valid (returning an int).
      foo(baz); // Valid (returning a void).
      varfoo(bar); // Valid (assigning an int).
      // varfoo(baz); // Invalid (assigning a void (why???)).
  }