You don't actually need your own driver, you can just use the CDC device class.
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.
Readit Newsnanolith commented on We X-Rayed a Suspicious FTDI USB Cable eclypsium.com/blog/xray-c... · Posted by u/aa_is_op
nanolith commented on We X-Rayed a Suspicious FTDI USB Cable eclypsium.com/blog/xray-c... · Posted by u/aa_is_op
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.
In libc, you can use setvbuf to change the buffering mode.
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.
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.
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?
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.
> 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?
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...
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
Have you made any of this work public?
It sounds really interesting.
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
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.
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.
This sounds awesome. Did you ever filmed it working?
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.