HackerLangs
TopNewTrendsCommentsPastAskShowJobs

nanolith

1,366 karmajoined 12 ปีที่แล้ว

comments

nanolith
·7 ชั่วโมงที่ผ่านมา·discuss
Wait... wasn't it already understood that relativity influences electron orbits of heavy elements? I clearly remember being taught some of this in physics, in the mid-noughties.

For instance, we know that gold gets its color from relativistic effects.

https://physics.aps.org/articles/v10/s3
nanolith
·4 วันที่ผ่านมา·discuss
I spent some time this evening beating the dungeon. It took a bit of time to get my head around the syntax, but once I found the tutorial, it clicked.

The game reminds me quite a bit of The Little Prover and The Little Typer.
nanolith
·9 วันที่ผ่านมา·discuss
If the flavors are permanently dead, it would be fitting if the grave markers included recipes for those mourning the loss of this flavor and who wish to recreate it at home.
nanolith
·11 วันที่ผ่านมา·discuss
Fair enough. I use my fiber library for cooperative multitasking, as an alternative to async I/O. It's still non-blocking, but as far as user code knows, it behaves as if it is blocking.

To do this, I disable signals on threads that are fiber threads, and instead rely on a signal thread to intercept signals and alert the appropriate fibers.
nanolith
·11 วันที่ผ่านมา·discuss
> For example, Boost uses ucontext as part of its fiber implementation.

Maybe for the incredibly slow fallback, it does. Boost context and Boost fiber has ABI support for *nix / MacOS / Windows for x86_64 and ARM/ARM64. The overhead for a fiber switch using this support is about as heavy as a virtual function call. In comparison, ucontext is very heavy.

I wrote my own fiber library for C. I got the idea from an old implementation I saw that used setjmp and longjmp, which took me down the rabbit hole of figuring out how to do this more efficiently and with an improved margin of safety. I chose to follow Boost's example, and in fact, used some of their fiber switch assembler with attribution in my library.
nanolith
·3 เดือนที่ผ่านมา·discuss
There is plenty of room for debate over this advice. Prefer do notation if the effects of the flow are more important than the data structure, and prefer using Applicative style if the data structure layout is more important to understand than the effects to build it. In the example in the article, the software is easier to understand from the perspective of how data was acquired to populate the record. However, this isn't true in a general sense; often records are purpose built in higher level languages to reflect effects and constrain them.

Example: when using Parsec or similar, Applicative style is far easier to understand when examining how records are parsed. In this case, the records will likely reflect the AST, which in turn will reflect the grammar. The two reinforce each other: additional constraints on syntax will naturally flock to data constructors.
nanolith
·6 เดือนที่ผ่านมา·discuss
That's true. The only advantage of writing a driver in this case is if I wanted to add functions, such as a programmable level shifter.
nanolith
·6 เดือนที่ผ่านมา·discuss
I could spot the clone because I'm familiar with the form factor of the FTDI IC, and I'm familiar enough with the datasheet to spot the expected passives.

I'm not too keen these days with FTDI's reputation for manipulating their Windows device drivers to brick clones. So, while I'm familiar with their IC, I don't give them any more money. The next time I need a USB to serial cable, I'll bust out KiCad to build it using one of the ubiquitous ARM microcontrollers with USB features built in. Of course, this is easier for me, since I can write my own Linux or BSD device driver as well. Those using OSes with signing restrictions on drivers would have a harder time, unless they chose to disable driver signing.
nanolith
·6 เดือนที่ผ่านมา·discuss
In libc, you can use setvbuf to change the buffering mode.
nanolith
·7 เดือนที่ผ่านมา·discuss
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
·7 เดือนที่ผ่านมา·discuss
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
·7 เดือนที่ผ่านมา·discuss
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
·7 เดือนที่ผ่านมา·discuss
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
·7 เดือนที่ผ่านมา·discuss
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
·7 เดือนที่ผ่านมา·discuss
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
·7 เดือนที่ผ่านมา·discuss
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
·7 เดือนที่ผ่านมา·discuss
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
·8 เดือนที่ผ่านมา·discuss
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
·8 เดือนที่ผ่านมา·discuss
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.
nanolith
·10 เดือนที่ผ่านมา·discuss
I'm living with heart failure. I have 20-30 years before I'll need a transplant, if I live a perfect lifestyle and keep my other health issues under control. Due to my other health issues, I am not a good candidate for a human heart transplant. It's not that a human heart transplant would fail, but that when I'd be placed against others on the list for a new heart, my other health issues would reduce my priority such that there is always someone with higher priority to receive a heart, up until the point in which I'm no longer healthy enough to receive a transplant. There are far too few human hearts, and far too many people who need one. All that the transplant boards can do is give hearts to those with the greatest momentary need, with the best chance of surviving.

Xenotransplantation is one of the life lines I'm counting on. I'm hoping that, by the time I need it, the issues that we currently have will be worked out. I have zero ethical issues with breeding and eventually culling pigs in order to save human lives. I hope that there will be other, better, breakthroughs by then, but if not, the best I can hope for is that the pigs are raised in a sterile and enriching environment, and that the only bad day they have is their last day.