ahelwer

9 ms·

1.
by ahelwer 18d ago
You need root in order to overwrite sudo in the first place I think, but yes password replay attacks are real. This is why I think it is a good idea to get a yubikey and use PAM to require a physical user presence check to acquire root priv
2.
The changing role of finite-state model checking(ahelwer.ca)
4 points by ahelwer 24d ago|0 comments
3.
by ahelwer 8mo ago
An alternative reading of these comments is "I went to the casino and had a great time! Don't understand how you could have lost money."
4.
by ahelwer 1y ago
There is a strong Jevons Paradox effect at play here though, people generally have a set amount of wall-clock time (1 minute, 10 minutes, etc.) they budget to check their model and then find the largest model that fits within that wall-cloc
5.
by ahelwer 1y ago
That's very neat! I will look at Truffle. The TLA+ interpreter is definitely "weird" in that it does this double duty of both evaluating a predicate while also using that same predicate to extract hints about possible next st
6.
by ahelwer 1y ago
Hillel Wayne wrote https://learntla.com/ which is quite good! Leslie Lamport also has a webpage of other possible learning resources, including a video course he put together where he wears many strange hats: https:/&
7.
by ahelwer 1y ago
There are some proposals floating around to evolve PlusCal. Probably the most prominent is Distributed PlusCal[0]. There's a programming language lab at UBC which is also doing a lot of experimentation with transpiling PlusCal to Golan
8.
by ahelwer 1y ago
There has definitely been a focus on improving developer onboarding in the past few years! If someone's PR is rejected now that can be considered a failure of the process, something to be fixed. I think when TLA+ was mostly a product o
9.
by ahelwer 1y ago
Hillel Wayne wrote a post[0] about this issue recently, but on a practical level I think I want to address it by writing a "how-to" on trace validation & model-based testing. There are a lot of projects out there that have tri
10.
by ahelwer 2y ago
I think it is good that people put in a lot of effort to collect this in one place. The report opens with a very strong perspective: >The case against Stallman is clear, and yet the free software community has failed to act, in particula
11.
by ahelwer 2y ago
This series of books has always been aimed at people who want to implement the underlying systems. If you’re more interested in the application side of dependent types you might like the book Functional Programming in Lean by the same aut
12.
by ahelwer 2y ago
I worked through this a few years ago and it is wonderful, but I found chapter 9 on the replace function totally impenetrable, so I wrote a blog post in the same dialogue style intended as a gentler prelude to it. A few people have emailed
13.
TLA⁺ is more than a DSL for breadth-first search(ahelwer.ca)
9 points by ahelwer 2y ago|2 comments
14.
TLA⁺ Unicode support: Learning to work with others in open source(ahelwer.ca)
3 points by ahelwer 2y ago|0 comments
15.
by ahelwer 3y ago
Good way to describe it. I tend to see it occur on lists alongside The Art of War and The Prince , which have this weird reputation as titanic, dense tomes read by Serious Men but in reality are more like pamphlets that you can go throug
16.
by ahelwer 3y ago
This is a great passage but in a society taking climate change seriously carbon farming will unironically become a thing. Planting certain crops or using certain forms of composting to sequester as much carbon as possible on large areas of
17.
by ahelwer 3y ago
All modeling suggests that applying both of these tools together (incentives & disincentives) is multiplicatively more effective than applying either on its own. Taxing emissions means those emissions still happened.
18.
by ahelwer 3y ago
Go ahead and buy the land & oil rights to a large oil reservoir if you want to cash in on this hypothetical program. Paying off the oil companies in this way means the end of the oil companies. They get a one-time cash infusion but that
19.
by ahelwer 3y ago
It's an actual published paper you can read, not something KSR made up.
20.
by ahelwer 3y ago
If you're still committed to technocratic market-driven solutions to climate change there's the interesting idea of Carbon Quantitative Easing, essentially directly paying people to not emit carbon (read: pay oil companies to not
21.
by ahelwer 3y ago
It is be interesting to think of how a checker would work that detects monotonicity & deploys this theorem to check liveness properties. Maybe I'm just describing the TLA+ proof language! Also something to bring up at the next mont
22.
by ahelwer 3y ago
That's an interesting idea about a built-in ordered opaque value type. You should bring it up at the next monthly TLA+ foundation community call on November 14th![0] It would be interesting to hear peoples' feedback on it. [0] Det
23.
Wrangling Monotonic Systems in TLA+(ahelwer.ca)
67 points by ahelwer 3y ago|7 comments
24.
by ahelwer 3y ago
The shortest possible answer is that qubit states are modeled as two-dimensional vectors on the complex unit sphere. We arbitrarily designate two orthonormal vectors on this sphere as corresponding to classical states 0 and 1. If the qubit
25.
by ahelwer 3y ago
You're talking about the difference between a scientist making like $50-150k/year salary and entities making millions or billions of dollars a year in profit. These are in no way comparable.
26.
by ahelwer 3y ago
I hope this counts as productive feedback if the author of the blog is reading this - the post you put so much effort into writing truly deserves a better presentation experience than this: https://cdn.fosstodon.org/media_at
27.
by ahelwer 3y ago
Undergraduate physics hasn't changed much in the past two years.
28.
by ahelwer 3y ago
Using math to model a system instead of learning math qua math does wonders for ease of understanding. Derivates and integrals become easy if you're using them to model the relationship between position/velocity/acceleration.
29.
by ahelwer 3y ago
(am also on the spectrum) > neuro-typicals mistake my intent and refuse to believe me This is an idea I had to unlearn. We struggle as much understanding ourselves as understanding other people. When people react negatively to our behavi
30.
by ahelwer 3y ago
Time zones and shared language/culture disagree? Or if you think you can get a 90% margin on the competition with the same result, go start a company and see how that works out for you.

More ›