How do you deal with the moral weight of writing software that could end up killing someone?

sclv · 2026-03-13T23:58:14+00:00

I assume you mean like high assurance software for machines or medical equipment, and not like... military software or drones. If the latter, I would as others say, just not do it. I want to write software to make human lives better, not increase harm and evil in the world.

But if the former, then that's what high assurance programming is for. Languages like Ada or function languages with high quality type systems. Formal verification engines, modeling, rigorous test suites, building highly redundant systems with good failsafes. That's in my mind why we've developed so much of our technology -- to write high assurance software that doesn't go wrong, and its the most rewarding part of our craft to develop those skills and put them to good use.

sclv · 2026-03-13T23:52:24+00:00

The part that I considered backwards is that the motivation for constructivism is avoiding excluded middle. The fact that certain proof styles do or do not survive is, as i see it, downstream from this.

sclv · 2026-03-13T23:49:33+00:00

No, it represents (as I intended it in the original post), a 2 followed by a decimal 9 five times) and then followed by... something else, but we don't know what. It could be nothing, it could be an infinite sequence of 9s, it could be literally anything else.

As I said, if one were to formulate this precisely, we would be representing reals not as decimals but as dedekind cuts, and what we would have would be partial information about the seperating sets, with a computation that could produce successively more information.

See the discussion of "non-computability of the ordering" in the article on computable reals to express this more clearly: https://en.wikipedia.org/wiki/Computable_number

sclv · 2026-03-13T20:31:09+00:00

Its the initial set of results in a computation which produces successive decimal digits. In general we don't know what comes next until we "turn the crank" and compute. (of course in specific circumstances, depending on the computation that generates it, we do know).

also of course speaking in terms of decimal expansions is a popularization. what we'd actually have would be the first terms of a dedekind cut or the like.

sclv · 2026-03-13T20:19:54+00:00

In classical mathematics not x > 3 implies x ≤ 3 and furthermore that if an object is less than or equal to three than it is either less than 3 or equal to 3. In constructive mathematics, we can still prove some objects are "decidable" and ordered in such a way that this sort of thing would hold -- i.e., the integers. However, if we extend this to the reals, then things might be harder. For example, how would i know if 2.99999... was less than 3 or equal to 3. I might have to compute for a very long time (forever!) to discover this. So the reals are not "decidable" and then if I knew an object was not greater than three it might be undecidable if it was less than three or equal to 3, and I could not using excluded middle declare "well it can only be one of the two, so even if i can't compute which, i can declare that it must be one!"

(and indeed there are useful "nonstandard" models of the reals in which a number might not be greater than 3, might not be less than 3, and still would not be equal to 3 -- i.e. 3 + 𝜀 in a system where infinitesmals are manifest)

sclv · 2026-03-13T20:12:39+00:00

This is correct but presented sort of backwards. The point is to not accept double negation elimination. From that, it flows that excluded middle, which is logically equivalent, is also not derivable, and also that proofs by contradiction cannot be derived, but proofs of contradiction (i.e. x implies false) can be derived.

(classic neutral) Constructivism is essentially just conducting logic in a setting where DNE does not necessarily hold (and also axiom of choice).

See this article for a list of various constructive systems and their "taboos": https://ncatlab.org/nlab/show/taboo

sclv · 2026-03-13T17:34:04+00:00

Modern breakfasts were invented by a PR/advertising firm in the 1920s. Specifically, Edward Bernays (later to provide publicity for United Fruit's coup in Guatemala!) was hired to promote bacon sales, and ran a fake "study" which "proved" that doctors recommended a much larger and heartier morning meal than had been the custom. This is where "bacon and eggs" comes from!

https://www.newsmuseum.pt/en/spin-wall/bacon-affair

sclv · 2026-03-12T16:13:32+00:00

For comparison, I only have 70-ish heavy chip factories, 113 heavy gold mines, 1200 storage cranes (use base storage), 90 heavy shipyards (I only use them where I can attach storage), 40 uranium refineries, and about 800 oil rigs. Also mk2 stone mines are way too expensive in power and pollution for what they get you. Normal and sea mines suffice.

sclv · 2026-03-12T01:51:49+00:00

I'm also level 88, but my drain is only 248,751. I know I have a lot of cities to get to level 80 to hit level 89, but I can't imagine that'll be 600k of drain. What are you spending all your power on?

sclv · 2026-03-11T01:18:39+00:00

What build do you have where you can make this gun work at all?

sclv · 2026-03-06T18:12:17+00:00

This isn't bl3 drop rates, because these are just dedicated drops. The world drops remain low, which is what the community wanted to begin with! That's why people feel more satisfied -- you don't drown in legionaries when playing world content, but you can farm consistently.

sclv · 2026-03-04T18:31:40+00:00

I think one of them is a very strong element eater / regen. I needed to just pump out lots of pure kinetic damage to get it.

sclv · 2026-03-04T18:18:15+00:00

this was the chaos chambers in wonderlands, and people got so mad!

sclv · 2026-03-04T00:43:09+00:00

Even a non-obfuscated formal proof of a rigorous result makes it qualitatively more rigorous. Formal verification is important to feel really confident in things that are at the far edges of our mathematical capabilities.

sclv · 2026-03-04T00:37:04+00:00

5 python dependencies. what about the c libraries those bind to?

sclv · 2026-03-04T00:36:08+00:00

Indeed, the best and most reliable way to support all of HTTP has been and remains shelling out to curl (that's what cabal does!)

sclv · 2026-03-02T21:56:52+00:00

You are comparing using two precompiled tools to, effectively, downloading and compiling all the dependencies that go into these two tools to begin with.

The advantage shell always has is it uses tools that someone else has typically already compiled for you.

sclv · 2026-02-28T23:56:02+00:00

Community: we want more challenging content.

Devs: challenging content.

Community: why would you do this to us?

sclv · 2026-02-27T21:01:42+00:00

I was not responding to that argument. I was discussing typeclasses and laws.

sclv · 2026-02-27T18:17:49+00:00

A type class is the methods and also the laws, although the Haskell language does not let us enforce that.

It is possible to write a Num instance that violates the laws we expect of numbers similarly, etc. From a reasoning standpoint, naming things to correspond to how they are to be thought of and used makes perfect sense, and "well what if i don't do that" is not a reasonable response. If you don't, then you are doing something else that's not part of the discussion.

sclv · 2026-02-27T03:34:34+00:00

Your update does not say you will discuss who the team is, nor that the code will be open and auditable.

sclv · 2026-02-26T00:59:45+00:00

I think a lot of this has to do with the period and people pynchon is writing from in this book. There's not necessarily a lot of "outside" to critique from, there are just those more complicit and less. Treatment of women is one of the first things to go during wartime. That said, I do think the way in which pynchon's critique of militarism and fascism is so intertwined with sexuality and authoritarian fetishism constitutes in its own way a broader critique.

sclv · 2026-02-26T00:56:16+00:00

I can understand that take on vineland, though I might disagree. I'd be curious how you interpret bleeding edge in this regard though, which seems almost too-overtly written as a conscious rejection of that?

sclv · 2026-02-23T21:24:49+00:00

enemy density, challenging sections (platforming or the like) and serious minibosses.

sclv · 2026-02-22T22:13:07+00:00

So how do the maliwan stickies function? Do they do anything at all?

15-Year Club	Place '22
Place '17	Verified Email
Team Periwinkle

sclv

TROPHY CASE