Readit News logoReadit News
hirple commented on Can the language of proof assistants be used for general purpose programming?   proofassistants.stackexch... · Posted by u/wslh
hirple · 2 years ago
I've been interested in this question myself - and recently wrote a basic web 'microframework' for Lean 4 [1].

I've loved being able to use Lean's macro system to write JSX-like HTML:

  def header :=  <header class_="header">
    <h1>todo</h1>
  ...
Ironically I've come up a bit short on how to use dependent types to do anything more advanced than matching handlers' to route types, which Servant [2] can do fantastically already.

I would love to be able to write types that describe, e.g., assumptions made about external resources, so that I can prove that "assuming my DB has such-and-such a latency, my page will always render in such-and-such a time" or something similar - but it's a bit beyond me at the moment.

[1] https://github.com/alex-wellbelove/LeanServer [2] https://hackage.haskell.org/package/servant

hirple commented on UK expected to be only major economy to shrink in 2023 – IMF   bbc.co.uk/news/business-6... · Posted by u/open-source-ux
dTal · 3 years ago
[flagged]
hirple · 3 years ago
As a rule I find that people who take the common, simplistic, tweet-length view of British rule (i.e. that it became rich by stealing from India, that it was the deliberate invoker of India's famines, that it was racist even by its times standards, etc), assume that anyone who disagrees isn't aware of basic history.

I've also noticed that there's always an (annoying) triumphal 'gotcha' when they link to some short-form essay mentioning basic facts, denied by nobody, of the famines and loss of relative share of GDP suffered by India etc.

Again, _everyone knows this_. It comes across as naive and arrogant to assume otherwise.

The effect British rule had in India (and everywhere) was extremely nuanced, and there is a huge amount of interesting history to be debated. After all, we're talking about a subcontinent over a 350 year time period.

The British, for instance, banned the practices of Sati (burning widows alive) and of infanticide, and explicitly allowed Indians to compete on equal terms with the British in examinations to enter the Indian Civil Service.

There's very little consensus amongst historians whether or not they were responsible for the famines India suffered at the time, or if they even made any net money from India whatsoever, given their constant fear of raising taxes.

I'm not necessarily trying to take a position either way, by the way, just begging people who are nodding along to some of these bumper-sticker anti-colonialism comments to read more deeply into what is an unimaginably huge subject.

hirple commented on Paredit 25 released, after 8 years   paredit.org/... · Posted by u/salutis
srcreigh · 3 years ago
Same. I don’t even have shortcuts for paredit, I just M-X barf-forward- whatever (fuzzy find with selectrum) when I need it.

The only paredit shortcut I know is M-s to remove a set of parens.

That said I also use boon, which has some modal editing in particular a way to skip past an entire set of parens.

To GP: Why not enable it just for sake of keeping your parens balanced. Make sure you have a good way to discover commands like selectrum. And tada. Don’t have to learn it all right away.

hirple · 3 years ago
Somewhat related - does anyone use meow + paredit? I can’t find a clearly recommended way to combine the two as I can with boon.
hirple commented on The ‘liveaboards’ sailing away to a new life   theguardian.com/travel/20... · Posted by u/nigerian1981
matkoniecz · 3 years ago
I am pretty sure that

> We live on around £5 a day

from article is a big misunderstanding or a blatant lie.

But what kind of minimal funds are needed to pay for a boat, fuel, repairs, docking fees etc. Can it be cheaper than renting/owning flat?

hirple · 3 years ago
For canal boating, absolutely. Maybe 20-30k for a cheaper boat. Can moor for free. Coal and fuel maybe £100 a month each, depending on how much you travel/if you have solar etc. You do need to black your hull every few years, but they’re generally sturdy and don’t need much more than that.

Yachting, I have no idea.

hirple commented on Show HN: Two-way Jira sync in a collaborative spreadsheet and Gantt   visor.us/landing/visor-fo... · Posted by u/electric_muse
alephnan · 4 years ago
Has anyone ever done something similar, but with spreadsheets in Org-mode?
hirple · 4 years ago
I assume you've taken a look at org-jira?
hirple commented on Magit, the magical Git interface (2017)   emacsair.me/2017/09/01/th... · Posted by u/Tomte
StreakyCobra · 4 years ago
Tip of the day: you can have `magit` as a fast and standalone tool by using this script (require emacsclient to be setup properly):

  #!/usr/bin/env bash
  
  emacsclient -c --eval "(progn (magit-status) (delete-other-windows))"
This will open the repository under the current path in a maximized magit window.

The only downside I have for now about magit is when using `pre-commit` it can run for long sometimes, so it would be nice to see the progress/output of pre-commit while waiting for the commmit message buffer to appear. If you know a way I'm all ears.

hirple · 4 years ago
You should just be able to hit `$` in the magit buffer to watch the output.
hirple commented on New evidence that British workplaces are losing viewpoint diversity   ethicalsystems.org/new-ev... · Posted by u/gainof-function
zozbot234 · 5 years ago
> Leave it to the pub and Hacker News.

Actually, it would be nice if you left politics out of HN, too. In theory you could talk about politics and policy in a way that's conducive to intellectual interest and curiosity, but I've literally never seen this happen here with any consistency.

The political threads are always littered with knee-jerk hot takes that just don't belong here from an intellectual POV. To be very clear about what I'm saying, this is not about ideology; I've seen this behavior come from all parts of the political spectrum, and I find it even more annoying when "my" preferred side is doing it.

hirple · 5 years ago
I agree with you - but the standards elsewhere seem to be so much lower even than here that I think it's (possibly) worthwhile having political discussions on HN.

Of course, I would love to know of a place that discusses things even more sensibly.

hirple commented on What's Accenture? (2020)   retool.com/blog/whats-acc... · Posted by u/kgggvin
perardi · 5 years ago
That is savage.

And disturbingly accurate, as once you strip away the admittedly really quite nice typography from Accenture documents like this, you are left with just absolute pablum.

https://www.accenture.com/_acnmedia/Thought-Leadership-Asset...

(Edit: Wow, they apparently used the phrase “Thought Leadership” in this file name without irony.)

hirple · 5 years ago
Speaking as a consultant, these are terrible slides.
hirple commented on Ask HN: Why aren't we building a database of formally verified software?    · Posted by u/cloogshicer
hirple · 5 years ago
I guess Coq/Lean standard libraries fit this definition.
hirple commented on Whole school board resigns in shame after forgetting their WebEx call was public   theverge.com/tldr/2021/2/... · Posted by u/fireball_blaze
happymellon · 5 years ago
All schools here in the UK start at 9.

Why would you start your schools at 6am, I wouldn't take a job that made me start at 6am every day? I would just slowly get tired and less effective.

hirple · 5 years ago
Not true, we certainly have those that start at 8. Consider a ~45m commute and time to get ready, and waking up at 6 something is not unheard of. (I personally had to wake up at 5:45 to catch a bus to a school over an hour away).

u/hirple

KarmaCake day32November 26, 2020
About
CA. ML, formal verification.

email: hirple@corgi.coffee

View Original