We passed on Rust for Ada/SPARK2014 to write to bare metal on Cortex-M processor for real-time, high-integrity, and verifiable mission-critical software. Rust is making strides to be a future competitor, but it's new to the formal verification tooling and lacks any real world legacy in our domain. Ada's latest spec. is 2022. Other than AdaCore's verified Rust compiler, Rust still does not have a stable language specification like C/C++, Lisp, or Ada, SPARK 2014. I have no doubt that it will start rising to tick all the boxes that Ada/SPARK do right now with their decades of legacy in high-intetrity, mission-critical applications. The mandate to use memory-safe software put into effect this past Jan 1 2026 puts some wind in Rust's sails, but it's more than memory-safety in this domain. Plus, I do not enjoy Rust, but Cargo is nice. We're looking at Lean for further assistance in verifying our work. I think there was and is lot of Rust evangelism that will also carry it forward and boost even more Rust popularity,
Yes, and AdaCore's tooling is formally verified and produces reports already familiar to aerospace, railway, and auto auditors for verifying certifications making it attractive to this industry segment of high-integrity apps. Memory safety is taken care of mainly through the features Ada/SPARK2014 offer in creating safe, high-integrity programs, correct.
I've read (from one from one of the people that contribute to Rust afair), that they were involved building formal verification for Rust, and found that the control flow is just so complex that its very hard to use the language like this.
But I think the lack of a formal specification is really not as big a deal as it's made out to be. It's one of those "think of a technical reason to justify a decision I've already made" excuses.
Obviously it would be great if Rust does get a full formal specification but I think avoiding it because it doesn't is just silly. C++ has a formal specification... which frequently has bugs and ambiguities. They aren't magically right and either way you're going to need to do a lot of non-formal testing as well as formal verification if you want confidence in a design.
This is true even for domains where formal verification is routine like SystemVerilog. I've seen designs pass formal but fail in simulation or vice versa due to subtle differences in the semantics. (Hopefully that can't happen for Rust but you get the point.)
Rust is not really memory safe if you combine it with external libraries. Too many "unsafe" keywords, and lack of tooling for code analysis and verification.
Edit:
With c, you can do memory safety analysis on all system libraries and entire Linux kernel. Some OS kernels, libs and languages do not have dynamic memory allocation at all!
Some languages are memory safe!
Learn more about embedded programming!
To me Rust is just a nicer language than C. I don't care too much about how easy the language makes memory safety, provided it doesn't make it difficult. But Rust's type system, higher-order functions, polymorphism, macros, etc. make it more pleasant to write than C for complicated programs.
I'm going to download and check out Mine and Coalton. Right now, I use Neovide and Lem interchangeably. However, I am in deep with Shen. I bought a hardcopy of The Book of Shen, 5th Edition, and I still have Peter Kogge's 1991 text, "The Architecture of Symbolic Computers". I suspect the Hindley-Milner type system in Coalton will be more familiar to the Haskellers out there, but it is not as strong as Shen's Sequent calculus type system. In Shen, computation is allowed in side-conditions (if, let, and, etc.), so you can compute over terms inside types. Shen wins for raw expressive power and programmable types. Shen is very portable, but being a DSL, Coalton must integrate nicely with Common Lisp. And you get native exe's. Glad to see a simple way for people to program in CL or Coalton without having to go through the decades I have done with Vim and Emacs. VS Code bores me, but it is practical, even if it seems like junkyard truck with everything bolted on or hanging off of it.
I ran Minix around 1991 on my Amiga computer. Minix had a smaller attack surface and isolation provided by its microkernel vs. Linux's monolithic kernel. I had the Minix textbook, and it was easier to think about it because of the split along modules. I personally think Minix vs. Linux was very similar to Betamax vs. VHS. Betamax was technically superior, but the market picked VHS. I may run Minix again on my old Lenovo T430u from 2012. I was amazed that some of the code to Minix was in the appendix of the book, sort of like the magazines with pages of code to hand type in games or toy programs. I guess I liked MS-DOS for the same reason: tinkering, from my PEEK and POKE back in my Commodore PET 2001 (1977) and Vic-20 days...
Betamax had better picture quality but only had 1 hour of capacity. VHS had 2 hours. Consumers preferred not having to switch tapes to higher picture quality.
Convenience is a technical advantage. That's why streaming later beat Blu-ray despite a regression in picture quality.
From my comment below, we used Betamax back in 1982 for film class and would go back to editing it on a tape-to-tape deck, so starting with Betamax vs. VHS meant you had less degradation in the final edited product, since you started with higher quality. Sort of like editing RAW vs. JPEG photos nowadays to start with more resolution/information. For me streaming vs. my Blu-ray stuff was about cost. A $39 Blu-ray disc vs. a $12 movie or free movie with subscription. Amazon Music took away a purchase I had from 2014. I could no longer download it, since something changed with their licensing agreement. I have digitized my DVD/Blu-ray discs, since the discs don't last forever. I keep a streaming rez and a hi-rez copy of my faves.
Surely you'd just make the tape/cassette larger? Remember laserdisc?
I remember watching something on Betamax, possibly Star Wars but have no recollection of changing tape. My dad was a teacher and had access to a VT player on my birthday. On other occasions he would bring home a BBC Microcomputer. Quite a treat when we couldn't afford to buy our own TV even.
> Surely you'd just make the tape/cassette larger?
Originally, Betamax increased physical tape length, but cutting tape speed (like how vinyls can play at different RPMs) was a more economical way of cramming more hours onto the same tape by cutting quality.
Both VHS and Betamax went through multiple phases of this. Eventually VHS won by being cheaper.
I thought this was true for a while, but it seems to be a side effect of Betamax being more expensive in general.
The counterexamples that convinced me were Grok and Steam VR aren't taking significant marketshare from ChatGPT and Oculus despite having better support for adult content.
Originally, I thought this would kill Oculus given that's the most popular use of VR, but nope.
Porn tech usage is driven by solving some problem from the previous generation.
Videotape solved the "can't watch film porn at home" problem. Online payments and delivery solved the "need to risk going to the store to buy porn" problem.
What does VR porn solve over just watching standard porn on your monitor/TV?
And because of the resolution limitations, aren't VR headsets actually worse for watching porn than modern 4K monitors?
Well, interactivity was solved by OnlyFans, no? And OnlyFans seems to butcher video quality pretty badly yet it doesn't seem to dissuade people very much.
Yes - VHS had limited luma bandwidth that was about 50% of broadcast TV, and extremely limited chroma bandwidth (the equivalent of about 40 pixels per line). There's a reason laserdisc existed.
Spot on...as I recall, you really couldn't tell the difference between VHS and Betamax unless you had a studio-grade CRT. Well...that's probably unfair...you could tell an difference, but not an enormous difference. It wasn't like going from 480i->1080p; not even to 720i. On our old analog TV there wasn't remotely enough 'wow' to justify the price difference and other limits, so dad took back the BM player and got a VHS.
Yes, but you're forgetting editing wasn't digital/digitized. You would copy from one tape to another, so a degradation issue. It's not the TV's capabilities, but if you started with higher quality you would get less overall degradation. I took film classes in TSOA at NYT back in 1982, and one class was film production and the other was lugging around a huge deck and camera in Betamax and then going back to a tape-to-tape transfer editing deck.
Well, sure. My point is, as a consumer product, betamax did not deliver on its promise to the consumer that bought it. It's really not important at which stage of content production and distribution the promises got lost (and I think you might be underappreciating 'most people's TV set was pretty meh', especially after the components had some life on them). It was sold to my amateur audiophile dad (yes, we had a reel-to-reel) as 'world changing video', and it wasn't, certainly not at the price point. I think the obvious superiority at the content production phase is testified to by the crazy longevity of BM in that niche, but since we couldn't really see that in our house, we (and almost everyone) bought the VHS.
A delta of 3 bpm on sauna days corresponds to around 4% delta if the baseline is 72 bpm. I've gone from a resting heart rate over a 7-day average of 64 bpm to 58 bpm by jumping 15 min. of rope a day, 4 times a week. I've lost weight, body fat, and I feel like my body is more efficient with corresponding lower heart rates throughout my active day. I like saunas for recovery and aches, they put me in a relaxed state after, and I believe the dilation is flushing my system. Like anything else, moderation. Perhaps I will add sauna to my weekly routine 1x per week or less.
PSA: if you like saunas but don't have easy access to one, those IR sauna bags you can buy online work great.
Some people find it gross to basically sweat inside a powered sleeping bag, but if you don't mind that you can get the same effects of a sauna while lying on your (covered) couch and watching YouTube.
Wow, they look really quite dangerous. I wouldn’t want to pass out in one. Yeah you can pass out in a sauna too, but it feels easier to lurch for the door than to fight with a sleeping bag.
There's a timer shutoff. I know I can sit in mine for the full hour at the highest setting, so it's not anything my body can't handle. You can set it for less time at a lower heat setting, too.
Everytime I start jumping rope after a long break like Winter. It immediately starts trending lower a few points in 3 to 4 days, and plateaus after 6 weeks or so. I've averages as low as 54 bpm, but not as consistent as 58 to 60 bpm over a six month period. Granted, I tend to sleep better, have lower stress anecdotally and quantifiably by my Garmin watch's data. It has to be said that I usually add more exercise, because the rope jumping greases the skids so to speak. Good begets good.
Since it's not a battery storage setup, the energy being sent into your home circuit alleviates demand by a small amount. Where did they come up with 10 to 25% savings? Factors such as an optimal view of the sun for as much as possible, south-facing or biased East or West, would be the max. payoff. Night would be a zero net gain. At a savings of $7 a month, the panel would pay for itself in maybe 10 years not factoring in government subsidies. You need to keep it clean as well for it to maintain its potential output.
Stuff like your fridge can use a fair chunk of power continuously and a small solar setup can offset that when the sun is out. Same with routers, chargers, standby devices, TVs, etc.
For a 800W setup, 4–5 kWh on a very good summer day is plausible. Over a full year, it's going to be something like 600–900 kWh depending on orientation, shading, and location. So in strong summer months you might get something like 80–120 kWh. But you won't be able to use all of that unless you have a battery.
However, A typical apartment in Germany is not using that much electricity. Roughly speaking, a one-person place might use around 160 kWh a month and a two-person place around 270 kWh. Finding a use for 20–30 kWh a month during sunny periods. That's how you get to 10%. 25% might be harder but doable if you could somehow have a battery soak up the excess power. I don't think there are a lot of plug and play solutions for that yet. But it should not be that hard to do technically.
Power in Germany is relatively expensive 160*0.40 is about 80/month for me. I pay a bit less than that because I use less power somehow. But still, that's is close to 1000 euro per year. Saving 100 per year means the whole setup would earn itself back in 2-4 years (most plug and play setups you find on amazon are between 200 and 400 euro). And depending on where you live you can actually get some of that back via subsidy. But it basically pays for itself even if you don't. Unless like me your balcony faces east and you only get a few hours of sunlight in the morning.
Wow, 160 kWh/month! My family of four uses as much as 790 kWh/month in the high-heat or very cold season, with an annual average of 650 to 700 kWh/month. We pay around 0.13 USD/kWh, however, when you add the taxes and supply charges, it actually averages out to 0.28 USD/kWh...Granted I have two younger children at home, and my wife cooks fresh meals all the time - fresh-baked breads, etc., so we don't eat out much at all. We have an electric oven, electric washing machine and dryer, and electric cooling and heating (split unit HVAC).
I did really rough math and a hypothetical 200W panel getting 100% sun for 5 hours per day (1 kW/hr) would net you a whopping ~$9.30 in savings per month. We're paying something like $0.31 per kW/hr in NYC and it's a lot of money right now.
Did your calculations account for the suboptimal angle of the panels in most balcony solar setups? Most calculators assume the panels are at an optimal angle or on a roof pitch, not vertical like the image in the article.
A setup like the image in the article is going to get much lower than optimal efficiency because the panel is mounted vertically. She could be netting closer to $2-3 dollars per month or even less depending on which way she’s facing.
Yes, and I think it's important to highlight that Iverson would write APL on chalkboards and paper when working on math at times. I am sure some people here can hand write a program, but it seems so much more akin to writing math. I am in J daily, APL once in a while, Uiua more frequently, but J is the only one I actually write in my journal and then try it on my J phone app or when I open up my laptop. The intro books for J are great for working through math and learning J - Concrete Math for Computing in J; Easy J; Calculus; Arithmetic - https://code.jsoftware.com/wiki/Books
Yes, a strong argument, and staying in a line of PLs: F# for high-level, and F* <-> Low* for theorem proving and low-level coding. I am evaluating F/Low for verified code on Cortex M processor that I am currently trying to write SPARK2014. The Cortex A processor is running seL4 for less safety-critical tasks. I did look at Lean4 as a scratch for my Idris2 itch use cases.
Looks great! Nice work.
I am steeped in CAD for my work flow, so I used to program AutoCAD in AutoLISP, Rhino in Rhinoscript, now F#, and FreeCAD in Python as well as Blender. They have the geometry engines built-in and tested over decades. I think this is good for the maker with a 3D printer to do parts that are relatively simple (not discounting parametric code to make complex shapes here). Industry needs integration of CAD, BIM, CAM, Viz, etc. Take a look at this now older (2014) project where Rhino and F# were used to design and manufacture complex geometry for a real world build: https://www.youtube.com/watch?v=ZY-bvZZZZnE
Agreed. When you zoom in, even the normal life stuff can give you concern. I showed my kids what creatures live on their and others' bodies. You have millions of microscopic arachnids called Demodex mites living in your hair follicles and sebaceous glands, particularly on your face. My wife gave me an evil look as I showed my children this fact in online vids and pics. Granted these are symbiotic/parasitic relationships of life, but still, the closer you look, the more you see!
Correct, not millions of Demodex mites, which are usually in the hundreds to thousands on a typical, non-infested human. The millions should be the general amount of mites and other symbiotic/parasitic on and in your body. Thanks!
I have loved math since I was a child, and I think it depends on when you grew up and how steeped you are in reality vs. the virtual or the computer world, and how much of an abstract vs. concrete thinker you are. I was always making things in modeling clay, that greasy grey-green stuff, and so my scale was what I could make out of one brick of such stuff. I bought my first computer in 1977 (Commodore PET 2001), and the CBM ASCII set had some graphics, but nothing compared with today's graphics. My first encounter with visualization and scale was writing a program to let me know which of the four moons of Jupiter I was seeing in the sky that night. Io, Ganymede, Callisto, and Europa's orbits are almost edge-on to our view from earth, so I made Jupiter a capital O, and the moons were lowercase letters. I printed this out on a thermal printer (like a wide receipt). Cosmos was the rage on TV and I had read Einstein's Universe by Nigel Calder. I had a telescope and a microscope, so the micro and macro were very real to me. I suspect if you grew up on tablets and only built things on a 3D printer scale, you don't have that unbridled sense of the small and large except on very abstract terms. However, not a donut, not a universe-scale torus, but rather a pool donut comes to mind when I first hear torus!
I built an XYZ router table in the early 2000s out of old stepper motors. It was 8'x4', and I built stitch-and-glue wooden kayaks from the panels I cut on it. These would wind up being 16 to 22 foot long kayaks to go into the real world and have fun!
reply