Readit News logoReadit News
nanolith commented on I'm just having fun   jyn.dev/i-m-just-having-f... · Posted by u/lemper
ericmcer · 3 days ago
That still feels a bit off, as you are "having fun" because it ultimately is the road to success.

There is a deeper hurt in the tech world, which is that we have all been conditioned to crave greatness. Every employer tries to sell us on how important what they do is, or how rich everyone will become. We can't even vacation without thinking how much better we will perform once we get back. That struggle with greatness is something every human grapples with, but for workers in tech it is particularly difficult to let it go. The entire industry wants us to hold onto it until we are completely drained.

Anyway the result is sentiments like this, where having fun, exploring and learning can't just exist for the inherent rewards.

nanolith · 3 days ago
As per my original comment, these examples are only indicative that profitable endeavors can come out of these things in unexpected ways, but that's not the point of doing these things. I'm never going to profit from, nor recoup the costs I've sunk into most of the mad science I do. That's not the point. I do it because it's fun and because I like building cool things.

These examples are one justification for why we should embrace these kinds of hobbies, and not the desirable outcome for these kinds of hobbies.

nanolith commented on I'm just having fun   jyn.dev/i-m-just-having-f... · Posted by u/lemper
lo_zamoyski · 3 days ago
Josef Pieper wrote a book called "Leisure: the Basis of Culture"[0] - published in 1948 - in which he discusses the meaning of leisure, which is not what we mean by it today, and criticizes the "bourgeois world of total labor" as a spiritually, intellectually, and culturally destructive force.

Today, we think of "leisure" as merely free time from work or recreation, something largely done to "recharge" so that we can go back to work (in other words: modern "leisure" is for the sake of work). This is not the original meaning. Indeed, etymologically, the word "school" comes from σχολή ("skholē"), which means "leisure", but with the understanding that it involves something like learned discussion or whatever. (Difficult to imagine, given how hostile modern schooling is, resembling more of a factory than a place of learning.) The purpose of work was to enable leisure. We labored in order to have leisure.

What's also interesting is that unlike us, who think of "leisure" in terms of work (that is, we think of it as a negation of work, "not-working"), the Greeks viewed it in exactly the opposite way. The word for "work" is ἀσχολίᾱ ("askholíā"), which is the absence of leisure. The understanding held for most of history and explains why we call the liberal arts liberal: it freed a man to be able to pursue truth effectively, and was contrasted with the servile arts, that is, everything with a practical aim like a trade or a craft.

This difference demonstrates an important shift and betrays the vulgar or nihilistic underbelly of our modern culture. Work is never for its own sake. It is always aimed at something other than itself (praxis and associated poiesis). This distinguishes it from something like theory (theoria) which is concerned with truth for its own sake.

So what do we work for? Work for its own sake is nihilistic, a kind of passing of the metaphysical buck, an activity pursued to avoid facing the question of what we live for. Work pursued merely to pay for sustenance - full stop - is vulgar and lacks meaning. Sustenance is important, but is that all you are, a beast that slurps food from a trough? Even here, only in human beings is food elevated into feast, into meal, a celebration and a social practice that incorporates food; it is not merely nutritive. Are you merely a consumerist who works to buy more crap, foolishly believing that ultimate joy will be found in the pointless chase for them?

Ask yourself: whom or what do you serve? Everyone aims at something. What are the choices of your life aiming at?

[0] https://a.co/d/eCd0cJX

nanolith · 3 days ago
That is an excellent way of considering both leisure and work, and certainly, a testament to the importance of studying the humanities.

Aristotle famously developed the Greek concept of εὐδαιμονία (eudaimonia), which dovetails into what you wrote. Roughly, the concept translates into "human flourishing" or "living well". While Aristotle's conception of what best constitutes this differed a bit from more ancient Greek concepts passed down through their oral tradition, and definitely differs from what we may consider today, it bears investigation. I definitely think that education and personal research fits into my conception of it, but tastes differ. Nietzsche gave what I considered some excellent responses to Aristotle, especially when it comes to finding / making meaning in our lives with respect to the modern world. The Transcendentalist school, in particular Henry David Thoreau and Ralph Waldo Emerson, also provided some interesting flavor.

I think that your questions should be asked continuously. We should all adjust our life trajectories based on our own flourishing, in ways that challenge us and lead to growth. There aren't clear answers to these questions. In fact, they should lead to a bit of discomfort, like sand in one's clam shell. Much as this sand will eventually form a pearl, these questions should drive us to better ourselves, little by little.

nanolith commented on I'm just having fun   jyn.dev/i-m-just-having-f... · Posted by u/lemper
xxr · 3 days ago
> The founder of FedEx actually wrote a business pitch paper for an overnight shipping company. This paper was given a low grade by his professor. He went on to form this company, which become a success, despite this low grade.

Was the paper given a low grade because it was a bad idea or because Fred Smith wrote a bad paper? If his pitch didn’t work, did feedback from the professor help Smith sharpen his idea so he was in a better position to make FedEx a success?

nanolith · 3 days ago
Allegedly, it was given a lower grade due to it not being a feasible business plan, in the professor's estimation. Of course, this forms part of the legend behind Fred Smith and FedEx, so that should be taken with a grain of salt.

https://finance.yahoo.com/news/fred-smith-told-yale-professo...

nanolith commented on I'm just having fun   jyn.dev/i-m-just-having-f... · Posted by u/lemper
nanolith · 4 days ago
We need more people in this world willing to do their own thing, even if others might find it intimidating or silly. The important thing is to have fun and learn things. Compiler hacking is just as good as any other hobby, even if it's done in good jest.

Sometimes, these things become real businesses. Not that this should be the intent of this, but it shows that what some consider silly, others will pay good money for.

Example: Cards Against Humanity started as a bit of a gag game between a small group of friends and eventually became something that has pop culture relevance.

Example: The founder of FedEx actually wrote a business pitch paper for an overnight shipping company. This paper was given a low grade by his professor. He went on to form this company, which become a success, despite this low grade. I like to think that he did this out of spite, and that Christmas letters to his old professor must've been fun.

nanolith commented on The Coming Need for Formal Specification   benjamincongdon.me/blog/2... · Posted by u/todsacerdoti
CoastalCoder · 12 days ago
Have you made any of this work public?

It sounds really interesting.

nanolith · 12 days ago
I'm starting to. One of the libraries I've started on recently is open source. I'm still really early in that process, but I started extracting a few functions for the optimized single and double linked list containers and will be moving onto the red-black and AVL tree containers soon. Once these are done, I should be able to model check the thread, fiber, and socket I/O components.
nanolith commented on The Coming Need for Formal Specification   benjamincongdon.me/blog/2... · Posted by u/todsacerdoti
Animats · 12 days ago
The trouble with formal specification, from someone who used to do it, is that only for some problems is the specification simpler than the code.

Some problems are straightforward to specify. A file system is a good example. The details of blocks and allocation and optimization of I/O are hidden from the API. The formal spec for a file system can be written in terms of huge arrays of bytes. The file system is an implementation to store arrays on external devices. We can say concisely what "correct operation" means for a file system.

This gets harder as the external interface exposes more functionality. Now you have to somehow write down what all that does. If the interface is too big, a formal spec will not help.

Now, sometimes you just want a negative specification - X must never happen. That's somewhat easier. You start with subscript checking and arithmetic overflow, and go up from there.

That said, most of the approaches people are doing seem too hard for the wrong reasons. The proofs are separate from the code. The notations are often different. There's not enough automation. And, worst of all, the people who do this stuff are way into formalism.

If you do this right, you can get over 90% of proofs with a SAT solver, and the theorems you have to write for the hard cases are often reusable.

nanolith · 12 days ago
I have been formally verifying software written in C for a while now.

> is that only for some problems is the specification simpler than the code.

Indeed. I had to fall back to using a proof assistant to verify the code used to build container algorithms (e.g. balanced binary trees) because the problem space gets really difficult in SAT when needing to verify, for instance, memory safety for any arbitrary container operation. Specifying the problem and proving the supporting lemmas takes far more time than proving the code correct with respect to this specification.

> If you do this right, you can get over 90% of proofs with a SAT solver

So far, in my experience, 99% of code that I've written can be verified via the CBMC / CProver model checker, which uses a SAT solver under the covers. So, I agree.

I only need to reach for CiC when dealing with things that I can't reasonably verify by squinting my eyes with the model checker. For instance, proving containers correct with respect to the same kinds of function contracts I use in model checking gets dicey, since these involve arbitrary and complex recursion. But, verifying that code that uses these containers is actually quite easy to do via shadow methods. For instance, with containers, we only really care whether we can verify the contracts for how they are used, and whether client code properly manages ownership semantics. For instance, placing an item into the container or taking an item out of a container. Referencing items in the container. Not holding onto dangling references once a lock on a container is released, etc. In these cases, simpler models for these containers that can be trivially model checked can be substituted in.

> Now, sometimes you just want a negative specification - X must never happen. That's somewhat easier.

Agreed. The abstract machine model I built up for C is what I call a "glass machine". Anything that might be UB or that could involve unsafe memory access causes a crash. Hence, quantified over any acceptable initial state and input parameters that match the function contract, these negative specifications must only step over all instructions without hitting a crash condition. If a developer can single step, and learns how to perform basic case analysis or basic induction, the developer can easily walk proofs of these negative specifications.

nanolith commented on An SVG is all you need   jon.recoil.org/blog/2025/... · Posted by u/sadiq
tambourine_man · 13 days ago
This sounds awesome. Did you ever filmed it working?
nanolith · 13 days ago
Sadly, I did not. I have the source code on an old laptop somewhere. I was disheartened when I considered productizing it and discovered just how deep of a patent tarpit I was dealing with.

It's on my list to revisit in the future. At this point, most of the patents are coming up on expiration, and it would make for a great open source project. Hardware has gotten much better over the subsequent years; there are nicer lower power solutions with integrated Bluetooth LE as well as other low power wireless technologies.

nanolith commented on An SVG is all you need   jon.recoil.org/blog/2025/... · Posted by u/sadiq
nanolith · 14 days ago
Around 15 years ago, I built a barbecue controller. This controller had four temperature probes that could be used to check the temperature of the inner cooking chamber as well as various cuts of meat. It controlled servos that opened and closed vents and had a custom derived PID algorithm that could infer the delayed effects of oxygen to charcoal.

Anyway, of relevance to this thread is that the controller connected to the local wireless network and provided an embedded HTTP server with an SVG based web UI that would graph temperatures and provided actual knobs and dials so that the controller could be tweaked. SVG in the browser works nicely with Javascript.

nanolith commented on Problems with C++ exceptions   marler8997.github.io/blog... · Posted by u/signa11
dmpk2k · a month ago
Could you elaborate on the model checking? You have two codebases then (model and C), or something more integrated?
nanolith · a month ago
The function contracts are integrated into the codebase. Bounded model checking tools, such as CBMC, can be used to check for integer UB, memory safety, and to evaluate custom user assertions. The latter feature opens the door for creating function contracts.

I include function contracts as part of function declarations in headers. These take the form of macros that clearly define the function contract. The implementation of the function evaluates the preconditions at the start of the function, and is written with a single exit so the postconditions can be evaluated at the end of the function. Since this function contract is defined in the header, shadow functions can be written that simulate all possibilities of the function contract. The two are kept in sync because they both depend on the same header. This way, model checks can be written to focus on individual functions with any dependencies simulated by shadows.

The model checks are included in the same project, but are separate from the code under instrumentation, similar to how unit tests are commonly written. I include the shadow functions as an installation target for the library when it is installed in development mode, so that downstream projects can use existing shadow functions instead of writing their own.

nanolith commented on Problems with C++ exceptions   marler8997.github.io/blog... · Posted by u/signa11
muragekibicho · a month ago
Honestly, I thought the diatribe would focus on needless complexity.

The starting example is how I'd do it in C:

```

void f(const char* p) // unsafe, naive use

{

    FILE \*f = fopen(p, "r");    // acquire

    // use f

    fclose(f);                  // release
}

```

Wouldn't the simpler solution be ensuring your function doesn't exit before release? All that c++ destroyer stuff appears somewhat unnecessary and as the author points out, creates even more problems.

nanolith · a month ago
In C, you're correct. The problem is that, in C++, one must account for the fact that anything could throw an exception. If something throws an exception between the time that f is opened and f is closed, the file handle is leaked. This is the "unsafe" that Bjarne is talking about here. Specifically, exception unsafety that can leak resources.

As an aside, it is one of the reasons why I finally decided to let go of C++ after 20 years of use. It was just too difficult to teach developers all of the corner cases. Instead, I retooled my system programming around C with model checking to enforce resource management and function contracts. The code can be read just like this example and I can have guaranteed resource management that is enforced at build time by checking function contracts.

u/nanolith

KarmaCake day1334January 8, 2015View Original