skysight-inc/HackerNews huggingface dataset:
There's some nice literature. I got into the field 15 years ago and there were practically no good textbooks. Things are way better now: https://avigad.github.io/formal_methods_in_education/

Nielson & Nielson have the standard textbook in static program analysis that is used everywhere. But it's quite unfriendly as it's written using abstract algebra. They've recently released two textbooks that are much gentler. Actually, I'd say they are easy going and fun but still retain all the mathematical rigor.

They use program graphs, which are a bit less general but a lot easier to digest. They cover all major techniques, including theorem proving, static analysis, model checking, abstract interpretation, type and effect systems, etc:

- Formal Methods: An Appetizer https://www.springer.com/gp/book/9783030051556

- Program Analysis: An Appetizer https://arxiv.org/abs/2012.10086

There's also a companion website with some F# code. The second book, which seems still unfinished discusses how to implement program analyses using datalog. This speeds up development quite a lot. Otherwise, developing your own static analyzer is a lot of work.

My dream is to implement some kind of framework that enables quick DSL creation along with lightweight formal methods support to verify programs written in each DSL. I think restricted semantics is the key to make formal methods practical. Quoting Alan Perlis, "Beware of the Turing tar-pit in which everything is possible but nothing of interest is easy."
Seems unique and very fitting for the times. Excited to see this get out there!
"If you're just launching, your focus should not be on performance or how easy it is to dockerize but to figure out who your user really is."

I agree here but I should note that my main focus is spending less time debugging errors at runtime and in production, and avoiding errors in the first place. This is primarily why I use rust.

"Not sure the verboseness of either golang or rust"

Verbosity has nothing at all to do with implementing good, robust code. You could do it in python, rust, or another language. With certain languages you don't have to spend time writing guard code because it's handled natively by the compiler, type system, or both.

" dynamically typed languages (arguably) makes it easier to change things,"

They make it easier to change things, not necessarily correctly. With modern IDEs refactoring is not an issue.

"Many have imagined and built valuable stuff in interpreted, dynamically typed languages before you, by being more focused on overall structure and making sure it's strict and resilient. One really doesn't have to search far for successful applications that are certainly way beyond 1000 LoC and still iterate pretty quickly for their size."

I am aware of this, but I can't help but wonder if they would be able to iterate much more quickly knowing that the compiler and type system eliminate entire classes of bugs. Sure, you might be able to get to running code a little bit faster, but if you have to spend time guarding it and debugging runtime errors... is it really faster?

===

There seems to be this mindset that being fledgling startup means no time for silly things like types or compilation, etc, only iteration. If one actually does their market research and figures out who their users are and what they want, one should be able to iterate just as quickly in i.e. golang or another compiled language with a healthy ecosystem.

I have not worked at a FAANG company or a company even remotely the size of those companies, but I have created and maintained somewhat large ruby on rails codebases. Debugging runtime errors became my bane, especially when I could not guarantee that the persons writing the ruby code were following modern practices (or any practices at all). Not that I think compilers are perfect, but they -do- catch so many errors, some of which may have made it into runtime.
This reminds me of those "MyLife" low-lifes who mine the internet on everyone's "behalf" and then email people telling them they have a "negative reputation".

It's possible to remove yourself so that your name does not appear when someone searches on MyLife.com by making a tedious phone-call to their call-center in India, but then they email you EVERY DAY with offers to clean up your online reputation for some fee.

The vengeance griefer in the NYT story is obviously a deranged crazy, but one person can only do so much. The guy who started MyLife however, Jeffrey Tinsley, is a multi-millionaire who has successfully gotten venture capital funding-- and causes grief on an internet-scale.

I wish there would be more media take-downs of MyLife, Classmates, Radaris, other scummy operations. Even better, I would expect that GDPR rules put in place for the USA would put these people out of business?
Partly because I'm a car spaz (I seem to buy a different one every couple years), and partly because I'm now fully remote with no expectation of going back to commuting, so I'm barely driving 50-100 miles a month. Having a nearly 60K car sitting in the garage doing nothing but depreciating is not a great plan. It's my third car, I don't really need it in any case.
Well that is another bad analogy, and while I do find all income taxation to be unethical marginalize tax rates are not treating people differently, they are treating incomes differently.

To treat people differently you would have to start basing income tax rates on characteristics of a person, such as race, sexual identity, age or height (like in your previous analogy)

Saying all income from 0-50000 is tax X, and income from 50000-100000 is taxed Y is not treating PEOPLE differently, all PEOPLE are treated the same in that situation.

To be clear I am a supporter of replacing all Welfare programs with a Negative Income Tax. I would also be in favor of a UBI that was not funded with Income taxation.

I also support the abolishment of all Income based taxation replacing it with Georgism Single Tax System
There is a lot of content I have passed up on watching, because it required firing up an app on my phone, searching for the content, turning on the tv, finding the Apple Play icon. And some apps still don’t support AirPlay. And some work directly with my TV, and some only with Apple TV.

Vs just turning on the TV and flicking channels to see what’s on.
"Container" is a very overloaded term in this context.

Plugins run inside "host" applications. I do not know of any way to do this inside a browser. Running it inside a Docker-like container seems to have more or less zero purpose from my perspective.
Another option: the "reversing" challenges in infosec Capture The Flag competitions regularly require you to work out which constraints a program has implemented and then plug into Z3 or Angr to find a solution, that might be a fun way to learn.
IDFA can be reset but that doesn't achieve the intent behind resetting it unless you also happen to reset everything else (such as the other immutable identifiers you mentioned), otherwise the new IDFA will be linked back to you thanks to any other identifier that you didn't (or couldn't) reset, including "fuzzy" signals such as IP addresses or usage patterns.
I would recommend the book, Introduction to Logic by Irving M Copi and others. It has a large number of interesting exercises too.

Another choice would be the book, 'The Trivium: The Liberal Arts of Logic, Grammar, and Rhetoric : Understanding the Nature and Function of Language'
by Sister Miriam Joseph.
Comments on this from 5 years ago, just for reference: https://news.ycombinator.com/item?id=10308004
Equity markets are the new GoFundMe. You even get a chance at a return.
Not to bring up the usual debate again, but anyone trying to sell you one side of the static/dynamic debate without acknowledging that this is not a cut-and-dry issue is doing you a disservice and it is probably in your best interest to not listen to them.
I'm not clear: Is this proposing that we make risc-v CPUs that also perform the work of a GPU, or is this a way to make a risc-v GPU (standalone)?
I replied to another person who asked the same question. TL;DR: Reasons, none of which have to do with disliking the car.
I agree that person experiences are not exactly reliable, but I think it's also good to remember that they can have the appearance of facticity and accuracy, as indicated by the sentiment of the person you were replying to.
It's not 2-phase. It's split phase. But you can think of it as being 2-phase to make the math convenient.
Sounds like you may not be familiar with Django, but it's honestly an amazing option if you want something that's mature, stable, well documented and full stack (the latter being key - one of the only ORMs I don't hate).

The biggest problem for Django and Python in general to me is more in the line of the scalability (performance) question. You are simply forced to put one or even two layers in front of it with a multi-process architecture just to get it to a baseline deployable state (in this case, traefik + gunicorn). But the good news is there are so many people doing that it really isn't a problem. And it turns out you probably want that architecture anyway (probably best if your application server isn't also doing your TLS etc).
One of the best introductions:

https://forallx.openlogicproject.org/forallxyyc.pdf

Highly recommended. Also provides good preparation if you want to go on to study topics like non-standard logic and automated proof systems.
God is good.
My experience is it would be best to stay away from these things. God has helped me be psych med free since 2014 even caffeine, not mormon btw. For me, it was a lack of knowing what was better out there that encouraged me to take them, and finally ended up in a hospital needing all kinds of treatments for adhd/bipolar etc. Needing to recover from things that only 'bad people' did. Eventually with doctor's approval was how the medication was removed, after a person came and prophesied for me to stop medications, at a moment the Lord had impressed that it would happen, interesting long story [1]. I had to learn to lead an orderly life and work with doctors while in treatment. It's really nice to be free from the illness and the meds, though grateful for the meds (at the end it was only a small amount of haldol vs lots of zyprexa at the beginning) when they were needed, However it can be an encouragement in the Lord Jesus to people.

[1] https://soundcloud.com/brianlovejesus/testimony-of-jesus-wor...
This feels very hand-wavey to me. I can patch and ship my docker images the same way I might patch a server.

apt-get update && apt-get upgrade

rinse, repeat.

Secondly, all this cargo-culting around small containers is fine if you are cramming resources. I am not.

The reality is that my projects and many others are really, really over-provisioned. Looking at my graphs right now, I am on the front page of HN and my server load is still only 20%.
A lot of sports streaming requires a cable subscription, to even be allowed to stream the content.

Except the games that are streaming only, and you can’t watch on cable.

It is very consumer hostile experience.
This is my left hand and this my right.

I have to save that kid that fall into the well.

Let your mind free and ...
I am wondering the same.

Maybe everybody is kinda hoping for the short squeeze? WSB is to stick it to the man but the other market participants?

The stock is shorted above 100%. If the price goes up enough, maybe the shorters will be have to exit their position and then will be the one left bagholding?

It really depends at which price they started the short. $8, $20 $350 $450?

But the puzzle is that "retail" is only a third of the market. a lot of the after hour kept it above 300 on Thursday and on Friday, and that is not the John Q Public doing those trades, so the big fish seem to be in agreement that it might be worth a try to go for the squeeze?
That’s just peephole optimizations though.
best thing ever for my chronic depression was a hit of E at a furry con, it basically kicked me out of a loop I'd been in for years and I've never been back in it since.
> but lisp syntax... is less legible than TLA+ imho.

I've developed theorem provers with more natural syntax, and in retrospect simpler grammars are better. The stone cold truth is that most people aren't interested in using theorem provers directly; instead, they're programmatically generating queries. Simpler grammar = easier to generate, and that out-weighs direct usability.

In my next system I'll be supporting both types of grammars in the parser.
I want to get notified every time a program performs any type of I/O system call. I want to see the parameters and the data being copied. I also want the opportunity to cancel the system call and even return fake results and data back to the program.

I already use strace to understand what programs do but it would be great if I could also intercept these calls in real time. Just keep the program waiting until I approve its open system call on that specific file.
I've seen and worked with developers that either didn't know, got paid to not know, or naively believed Facebook's bullshit about how their SDK is supposedly GDPR compliant.
Pretty sure Fox Sport is one of the Fox properties not included in the sale?
> Many have imagined and built valuable stuff in interpreted, dynamically typed languages before you, by being more focused on overall structure and making sure it's strict and resilient. One really doesn't have to search far for successful applications that are certainly way beyond 1000 LoC and still iterate pretty quickly for their size.

I once tried to get into a large Python project, and even the IDE (PyCharm) had trouble "guessing" the function parameter types. It's absolutely not scalable. I don't want to be reading a function and guessing "what the hell is the type of this?".
The problem is that it’s not free.. it’s probably $1000-2000 increase in parts to generate 50cents/day of electricity...
My MacBook powering my 4K monitor doesn’t look blurry at all, and I have it set to “2560x1440” scaling in the display settings.

It does however run a tiny bit slower due to that non-integer retina scaling.
I even have some difficulties figuring out what might distinguish 1971 as a landmark. In computing, it was a mildly impressive year seeing the introduction of coin-op video games (Computer Space), the general availability of floppy disks (while 1960s tech), Niklaus Wirth gave us Pascal as the latest in Algol-like languages, but not really that much out of the ordinary. (Well, the intel 4004 was introduced, starting the age of cost-effective Japanese calculators. But the 8008 was sketched out before that, relying on the late 1960s design of the DP 2200 – and it would take a few years before anyone took serious interest in that one.)
Only available in California, according to their website, which means it effectively does not exist. This is a product that’s been “coming soon” to the rest of the US since April 2019. Unless you live in CA you should include the high insurance costs into your estimate of TCO for a Tesla and treat “Tesla insurance” as a PR stunt.
Power to the people, I like it!
> It would also mean that no modern browser works any more since they need access to far more to even start up.

You are thinking again about old-style permissions control -- like SELinux. Yes, they are not going to work well, as you cannot really deny .cache access.

But this is not what we do in the modern system. You start a new mount namespace, and then mount a new tmpfs over /home. Then you bind-mount outside ~/.config/protected-firefox-profile to a ~/.mozilla inside the sandbox. And you expose ~/Downloads as-is.

And then you run firefox in that sandbox -- none of the system calls fail, any file which was written can be read back (sometimes only until the browser restarts), but your ~/.bashrc is totally safe.

You can improve this as much as you want. For example, want a private /tmp except shared /tmp/.X11-unix ? Sure. Want to hide your /etc and /var except few selected files? no problem.

This still assumes that there is a "sandboxed" and "non-sanboxed" parts of the account. You'll restrict more dangerous programs, like browsers, network clients, and games -- and leave things like text editors unrestricted, so there is no problems with editing text files.

Oh, and the thing that I am described are not some theoretical TODOs -- they are all supported and usable. I am running my own system made out of shell scripts and duct tape, but there are products out there like firejail [0] which implement all that.

[0] https://firejail.wordpress.com/features-3/#namespaces
> Your responses make it seem like you have never used a sandboxed app on the Mac, as every single thing you have mentioned has significantly better solutions than you are suggesting as an alternative. Even if you haven't, the things that it doesn't aren't a stretch to come up with and I might as well just list them here:

There's a reason that only a small minority of software can even run in such sandboxes without failing to work as intended or indeed pestering the user with dialogs for permission every second, and of many that can run in them, it's a security theatre that doesn't help if the software truly were malicious.

Are you running your text editor, terminal, IRC bouncer, or audio server in such a sandbox?

> This makes zero sense. If an app wants access to keylogging APIs, then it better be an app where it makes sense to be able to keylog other apps. 99% of apps have no reason to do this and have no need for full access.

There are, as said, far more things they need access to that can escalate to full privileges quickly:

- access to write arbitrary files owned by the user

- access to read from arbitrary ports that the user owns

- access to ptrace arbitrary processes the user runs

- access to edit the `PATH` of the user

> No, the alternative is that you give the application access to a file and now it owns that file.

Do you frequently use your text editor to edit one file, and one file only?

Give it access once to edit a script you wrote, now it owns the file; say it be malicious, it now changes the script so that next time it is executed, it allows for arbitrary code to run.

Not to mention having used it once to edit the initialization or environment variable files and user profiles.

> You can deny the browser the ability to read or write to the directory in general, but it may create new files and have permission to those.

In which case, it can exploit a race condition to replace a file that was created by something else immediately after the other software unlinks it to recreate it under the same name to trick the user.

It can also then create a symbolic link to trick other applications and gain write permissions of files it shouldn't have since almost no software is secured against such symbolic link attacks.

> Overall, it is eminently possible to make useful software, perhaps even most useful software, that operates under a reasonable sandbox.

It is, so long one be willing to forgo having basic control of one's system.

Android does it, as said, but in Android, the user does not enjoy such control, by design.
For years after I graduated from college I kept my old physics textbook next to my bed for exactly this reason. Interesting enough to easily pick a topic to read, dry enough to put me to sleep in a paragraph.
Race has nothing to do with sketchiness.
But why not though?
There's some pretty explicit stuff in there.

https://my90stv.com/#t91RVPnehDo
It looks like you could have C+GPU cores. I bet you could still split the gpu portion out into its own separate thing if you wished.
The goal of a startup is to build things quickly, so actually being able to build things quickly is important. If you know a set of tools well you can work quicker than using a perhaps better set of tools that you do not know well. That is an important point to make to people like me who like playing with new toys
This is only true for 4k monitors with MacOS. Anything under that looks terrible these days as it won't offer the HiDPI modes on those.
>"energy too cheap to meter" was first promised in the 1950s. We never got it thought.

Thanks Greenpeace.

Looking back with hindsight a few container ships worth of radioactive waste seems like a much better problem to have than an atmosphere with too much CO2 in it.
This is exactly how Spectrum and SiriusXM are as well. Easy to buy/upgrade, hard to cancel.
I don't see it that way. After multiple comments in one direction it was healthy to have someone say, "Wait a minute. Let's not forgot why we're here and what we're here to do."
It's designed with almost everything encrypted so that middleboxes can't inspect the contents of packets and filter or change them. This is essential, as it's been found that middleboxes now break almost every kind of experimental protocol that's not shielded in this way. So it's designed very much to resist ossification and allow protocol evolution.

Still, some vendors are adapting to QUIC by blocking QUIC:

https://www.fastvue.co/fastvue/blog/googles-quic-protocols-s...

Resolving the QUIC issue

The good news is that if QUIC communication does not work between a client and a server, the traffic will fall back to traditional HTTP/HTTPS over TCP, where it can be inspected, controlled, logged and reported on as usual.

At the time of writing, the advice from most firewall vendors is to block QUIC until support is officially added to their products. This recommended method will vary from firewall to firewall. Some firewalls allow QUIC by default while others block it by default, but all firewalls are able to allow or block it.

It's not really true that everything QUIC falls back to HTTP/HTTPS, as there are non-HTTP applications running over QUIC too. That kind of blocking is going to cause pain to the people I know who are implementing QUIC-only products. But it's not a new problem. WebSockets doesn't work everywhere either, even UDP does not work everywhere. HTTP is also a problem because some middleboxes modify responses (even if you don't care about privacy that breaks applications). The strongest fallback I know of in practice is HTTPS, but some places block HTTPS or modify the certificates, and some filter on the HTTPS domain which is visible in the TLS negotiation.
So can any device with Moonlight, I haven’t seen performance differences as far as local streaming goes between my Shield (2018 model) and my A1E (which has a fairly shitty SoC).
"apt-get update && apt-get upgrade"

You can do this exactly the same in alpine, with "apk update" and "apk add".

"Secondly, all this cargo-culting around small containers is fine if you are cramming resources. I am not."

The default docker python image is 885MB. python:buster-slim is 114MB which is much more reasonable. Even if you're not "cramming resources", pushing 885MB vs 115MB vs 20MB across the wire does add up over time.

In my case, we do quickly iterate and pull docker images so it does make a difference for my colleagues if the image is 30MB vs 500MB. Even if we're all on gigabit internet.

"Cargo culting" implies doing it without knowing why we're doing it. The benefits of reducing the size of docker images is apparent to everyone, although there are diminishing returns. With dive[0] it is very easy to figure out where the waste is.

"The reality is that my projects and many others are really, really over-provisioned. Looking at my graphs right now, I am on the front page of HN and my server load is still only 20%. "

Optimizing docker images has nothing to do with being over-provisioned.

I will concede that it's very different as a solo developer vs even a small team.

[0]: https://github.com/wagoodman/dive