Hacker News: jameshh

Using algebra and LLMs to verify a flight-plan bug fix in Lean

jameshh — Tue, 19 May 2026 04:07:02 +0000

Article URL: https://jameshaydon.github.io/algebra-llms-lean-flight-plan/

Comments URL: https://news.ycombinator.com/item?id=48189048

Points: 5

# Comments: 0

New comment by jameshh in "Solving `Passport Application` with Haskell"

jameshh — Sun, 29 Jun 2025 12:33:35 +0000

> the lack of parentheses for function calls plus currying means that to read a function call, you need to already know how many arguments the function takes

While I agree with the general sentiment of what you are saying, note that the syntax has nothing to do with it, it is purely about Haskell using currying excessively. The syntactic translation between Haskell and JS is straight-forward and 1-1:

    f x y z      ->  f(x)(y)(z)
    f x (y,z) w  ->  f(x)(y,z)(w)

I agree that excessive currying is not great, and generally push for non-curried arguments unless a curried form realy is used in practice. But for this to really be comfortable, and to still enjoy all the hgiher-order programming that's nice with Haskell, we would need good records (strucural, anonymous, extensible), which it doesn't really have right now, so we are stuck with currying.

New comment by jameshh in "Solving `Passport Application` with Haskell"

jameshh — Sun, 29 Jun 2025 08:54:45 +0000

I agree, I also renewed my passport recently and the website and process is quite smooth. It's the more complex cases, first requests from abroad, etc., that lack automation.

New comment by jameshh in "Solving `Passport Application` with Haskell"

jameshh — Sun, 29 Jun 2025 08:44:39 +0000

At least you got the bonus endscreen credits!

New comment by jameshh in "Solving `Passport Application` with Haskell"

jameshh — Sun, 29 Jun 2025 06:17:23 +0000

> although I don’t really see why it was relevant anyway, my son’s Britishness is derived from my Britishness, her nationality and the nationality of her parents is essentially irrelevant

This is essentially happened to me, the "75% of the initial doc requests turned out to be irrelevant" was referring to this sort of thing.

New comment by jameshh in "Solving `Passport Application` with Haskell"

jameshh — Sun, 29 Jun 2025 00:30:09 +0000

> I think the author may also be born outside the UK which may require other/more documents

In fact `applicant's father` (me) was born in the UK in this case, but `applicant's father's father` was not, the cause of the extra complications.

Solving `Passport Application` with Haskell

jameshh — Sat, 28 Jun 2025 23:01:15 +0000

Article URL: https://jameshaydon.github.io/passport/

Comments URL: https://news.ycombinator.com/item?id=44408872

Points: 308

# Comments: 125

New comment by jameshh in "UK air traffic control meltdown"

jameshh — Wed, 13 Sep 2023 06:41:25 +0000

For those of you still following this story, the flight plan that triggered the chaos has been identified!

https://chaos.social/@russss/111048524540643971!

> Tonight we were wondering why nobody had identified the flight which caused the UK air traffic control crash so we worked it out. It was FBU (French Bee) 731 from LAX/KLAX to ORY/LFPO.

> It passed two waypoints called DVL on its expanded flight plan: Devil's Lake, Wisconsin, US, and Deauville, Normandy, FR (an intermediate on airway UN859).

> https://www.flightaware.com/live/flight/FBU731/history/20230...

> Credit to @marksteward and @benelsen for doing much of the legwork here.

New comment by jameshh in "UK air traffic control meltdown"

jameshh — Tue, 12 Sep 2023 05:38:18 +0000

Thanks for this explanation. So, is the ICAO plan in some sense the "single source of truth", being the international standard and all?

New comment by jameshh in "UK air traffic control meltdown"

jameshh — Tue, 12 Sep 2023 02:34:05 +0000

> Bearing in mind this is likely decades old C code that can't be rewritten or replaced because the entirety of the UK's aviation runs on it.

It's new code, from 2018 :) Quote from the report:

> An FPRSA sub-system has existed in NATS for many years and in 2018 the previous FPRSA sub- system was replaced with new hardware and software manufactured by Frequentis AG, one of the leading global ATC System providers.

New comment by jameshh in "UK air traffic control meltdown"

jameshh — Mon, 11 Sep 2023 23:06:00 +0000

That's true, but then, why did engineers try to restart the system several times if they had no clue what was happening, and restarting it could have been dangerous?

New comment by jameshh in "UK air traffic control meltdown"

jameshh — Mon, 11 Sep 2023 02:18:55 +0000

That's super interesting (and a little terrifying). It's funny how different industries have developped different "cultures" for seemingly random reasons.

UK air traffic control meltdown

jameshh — Mon, 11 Sep 2023 01:08:16 +0000

Article URL: https://jameshaydon.github.io/nats-fail/

Comments URL: https://news.ycombinator.com/item?id=37461695

Points: 932

# Comments: 436

New comment by jameshh in "Radicle: A decentralized alternative to GitHub built on IPFS"

jameshh — Wed, 13 Mar 2019 11:25:35 +0000

> Conflict resolution doesn’t seem to be an issue for radicle as the owner of the repo (if I understand this correctly) is the one that needs to accepts patches and will have to republish on IPNS

This isn't quite what happens. Anyone who is authorised to do so (according to the semantics of the radicle code of the machine) can accept patches. They do this by forming a valid input (a radicle expression), with the correct signatures etc. This input is then sent to the owner via pubsub, so you are right that it is then the owner which republished on IPNS. The owner doesn't have to do anything manually though, this is all done automatically by the daemon. The assumption is that the owner will republish anything that is correct according to the machine's semantics, but it is true that the owner can censor otherwise valid inputs.

New comment by jameshh in "Elixir on Google Cloud Platform and App Engine"

jameshh — Wed, 24 Jan 2018 14:30:56 +0000

I think if you have an evolved enough type system, then there isn't such a problem. I have written an Elixir backend for Idris and given some examples of well-typed actor communication here:

https://github.com/jameshaydon/idris-elixir

New comment by jameshh in "Elixir on Google Cloud Platform and App Engine"

jameshh — Wed, 24 Jan 2018 14:29:38 +0000

I'm also making a backend for Idris: https://github.com/jameshaydon/idris-elixir