Maybe F* with dependent types and proof automation? I am programming in SPARK2014 currently and I would argue it is more of a Rust competitor with a longer legacy in high-integrity, safety-critical programming applications.
I've tried Idris. J and APL are great for quick analysis once you know them. I leave J open on my desktop for engineering and stats. Frink too for effortless units work. Haskell and its ilk are good for math. Programming to learn math works really well for some, since you work through a problem incrementally, especially with dynamic interpreters and REPLs. Pluto with Julia or Jupyter with Python or Mathematica too.
Me too, but I had a thing for Nastassia then when I was 18. Later, finding out how she was exploited by Polanski and others, I felt so bad for her. Hollywood is a dark place. I liked Tess, since I had read the Thomas Hardy novel in high school before seeing the film.
Thanks, I had looked at ATS many years ago, but I had forgotten about it. I'm going to look at both Lean and ATS, but I guess I'll stick with SPARK2014 for work now.
I have heard of Lean, but I just took a look for the first time. Certainly, much more Idris/Haskelly than the OCamlish F*.
Are there libraries available for general programming in Lean? Can you compile to another lower-level language like C?
I would be interested in writing some embedded code that could formally be verified. Right now, I have put some time in to SPARK2014, the subset of Ada.
Very well might be the case. I am speaking on old news. I would guess the lack of an official published standard makes it hard to create tools and support them over time - a moving target.
I shot competitively in JROTC and after, but never out to 1000 yards (914 m), only 500 yards. The Earth's rotation affects your trajectory significantly particularly if you are shooting longitudinally at a target at a higher or lower latitude. The Coriolis effect. I had more issues with varying winds or being consistent across shots.
Well, if we're nitpicking here, it is not 86,000s/day (24 hours * 3600s/hour) and 7.27x10^-5 radians/s, but 86,164.091s and 7.29x10^-5 radians/s.
24 hours is the time it takes the sun to return to the same spot in the sky due to earth having to rotate for another 3m56s to make up for angle gained by revolving around the sun in the same direction as the rotation of the Earth. This applies for the other planets that also rotate and revolve in the same direction - Mercury, Earth, Mars, Jupiter, Saturn, and Neptune. A sidereal day is 23h 56m 4.091s for distant stars to return to the same spot in the sky.
Damn, I knew that is why I botched my 6-stop exposure at my daughter's graduation! She can't blame me now! Thank you HN!
I just posted a relevant comment on the F* article a minute ago.
I would subjectively prefer F* because of syntax over Rust, but for the show control software we are developing, we are going with Ada/SPARK2014. Rust needs a formal, published standard like the other legacy PLs to draw the same crowd currently using Ada/SPARK2014 and the formal verification tools and some real-world safety-critical, high-integrity applications in its back pocket.
"I prefer F#/F* syntax, but I had to go with Ada/SPARK2014 for the safety-related control systems I am trying to verify formally and use for high-integrity applications. Rust is making some inroads with AdaCore and Ferrous Systems partnering on providing formal verification tools for Rust like they do for Ada/SPARK2014, but Rust still doesn't have a published standard like C, Common Lisp, Prolog, Fortran, COBOL, etc. Plus, the legacy is immense for Ada and SPARK2014."
I prefer F#/F* syntax, but I had to go with Ada/SPARK2014 for the safety-related control systems I am trying to verify formally and use for high-integrity applications. Rust is making some inroads with AdaCore and Ferrous Systems partnering on providing formal verification tools for Rust like they do for Ada/SPARK2014, but Rust still doesn't have a published standard like C, Common Lisp, Prolog, Fortran, COBOL, etc. Plus the legacy is immense for Ada and SPARK2014.
I was following this ever since I had read about AdaCore collaborating with Ferrous Systems on this, however, it is for the compiler. If they created a published Rust standard specific to their compiler then maybe, but I think there needs to be a general Rust standard comparable to other PL standards to start to encroach on the Ada/SPARK2014 world and a whole lot of real-world apps over time.
Yes, Carpenter made it to be about yuppies and unrestrained capitalism in 1988, however, art from the viewer's perspective 36 years later, can mean something different for that viewer or any other. Personally, I don't see the neo-Nazi and Jewish control of the world angle, but the way the media has sold the Palestine-Israel conflict, the passing of the redundant, free-speech-limiting, Antisemitism bill recently, and with thousands of Jews in the US and Israel protesting for a cease fire, and the thousands of police unleased on US college campus protestors, it can have a different interpretation. In 1985 Columbia students occupied the same hall for 3 weeks, and it led to Columbia's divestment from South Africa's apartheid regime, but most Americans under 35 or so, don't have historical depth. They sway in the wind of the media's hot air. For me, putting the glasses on or being red pilled, today makes the film applicable to a host of viewpoints, and not the cliche yuppy / capitalist trope even if that was sincerely John Carpenter's intention as an auteur. Sure, the acting is bad, and the late 80s coloring makes it seem a dinosaur to today's high-tech, SFX, CGI-addicted, chop-editing audience. I guess I am old. I love it. I also loved watching Wood Allen's 1973 film "Sleeper" for about the 7th time last month.
Is there a Rust standard yet like there is for C/C++, Common Lisp, and Ada/SPARK2014? Without that, it is a moving target compared to the verification tools that have been developed for say, Ada/SPARK2014. Not to mention the legacy of Ada/SPARK2014 in high-integrity, safety-critical applications from bare metal up.
Thanks, not really a blogger. I should really, since I have tried to pass down my experience or mentor, but unfortunately, a lot of people younger than myself, were intrigued but went on to chase safer and more lucrative salaried work. In Macau for instance, the government subsidizes the citizen residents with an annual stipend, free transportation, and medical care. One of my trainees after a couple of years left to take a government office job with benefits, and collect his $1k+ USD annual stipend. He remarked how much he learned, and how exciting it was to overcome his fear of being underwater, and how the new job would not really challenge him. But he still left it all behind. My older son picked up some of my eclectic background but has recently taken a tech job in software engineering. I am developing a protable, power dense, novel wirerope hoist with an old friend, and I am hoping it takes off and I can drag him into the business. There he can exercise many skills and still program. We are going with Ada/SPARK2014 for the high-integrity, safety-critical aspects. Rust hasn't standardized yet and doesn't have the verification tools yet, but it's heading that way. Maybe in 5 to 10 more years it will have a legacy in this field to compete.
Even though I started programming in 1978 (Commodore PET 2001), I avoided doing full-time IT or software work. It's always been adjacent to my work - embedded systems, CNC machines, robotics, animatronics - but I lost any appetite for going all-in after being an assistant DBA full-time for a couple of years. Computers and programming were always tools for me to use for other purposes. Troubleshooting code or wiring on a 45-ton underwater lift and then moving it just has a great payoff for me. I was a pressure junkie too. The show would have a technical fault, and it meant I was either jumping into a wetsuit and gear for a dive, or I was in the basement in front of a cabinet with thousands of wires trying to isolate and fix the fault while the audience grew understandably frustrated. Fortunately, we honed the system and these happened less frequently, but I have to admit in hindsight it really got my juices flowing.
I am currently working on a control system from low-level, bare metal to high-level HMI/GUI for a cool, new hoist primarily for shows, but with applications in other industries. Shooting for high-integrity, safety-critical certifications above and beyond similar machines. I have been doing electromechanical stuff since the late 80s/early 90s. Hydraulic, pneumatic, electro-mechanical, air muscles, etc. I did animatronics (Christmas windows back in the day in NYC). Before Arduino, I went from purely relay logic circuits to the Parallax Basic Stamp in the 90s to Pic chips, to other 8-16-32-bit chips. I am, we are, looking for an Ada/SPARK2014 software engineer/developer for this control system. Any HN'ers with SPARK2014 experience? I've reached out to AdaCore too. I have been a CNC and manual machinist (built my own CNC router table machine in 2002), welder, technical diver, industrial rope access tech (SPRAT certified). I am currently enamored with Cyber-Physical Systems (CPS) as something more than mechatronics. I have been riding motorcycles since the 80s, but now the highly integrated software on motos is next level. My current bike (2021 KTM Duke 890R) has power throughout the gears/rpms and amazing ride modes with supermoto ABS settings, and I am looking at the new Ducati 698 Hypermotard. The Ducati's software uses inputs and inertial motion sensors are integrated to allow beginner/intermediate riders to more confidently wheelie or do supermoto slide outs of the rear tire. Human-Machine Interface taking on a whole new meaning without the cyborg trope.
The House of Dancing Water in Macau. There is O at Bellagio, LV, NV, Le Reve closed at Wynn Las Vegas, The House of Dancing Water, Macau (where I worked), and there's another one in Wuhan, China (yes, Wuhan). The lifts had 8m hydraulic actuators to allow them to go down 7m and rise above pool level +1m. There were 11 stage lifts. The high-dive act was from 24m up. 17m liters of water.
I guess I am biased to like the article including it's presentation, since I spent 6 years as a technical diver fixing underwater hydraulics and electrical systems, but at much shallower depths than the undersea cables. A buddy of mine is an ROV operator for pipe-laying ships. Cool stuff, big stuff, and lots of crazy stuff involved (seeing weird, unidentifiable living creatures quickly and blurrily cross in front of the ROV's camera, etc.).
I remained hidden below water as a technical show diver, while 1800 to 2000 audience members topside were getting impatient with a "technical delay" show pause. Typically, we were checking for faults in safety systems on underwater lifts, or for a potential hydraulics leak. We'd exit under the audience seating and go back to work after clearing the issue.
In a world filled with high-tech desk jobs, finance, and non-tangible products, and having grown up working class, I have great respect for all the people behind the scenes physically keeping our tenuous world together. Some of this became readily apparent with once invisible food delivery and restaurant workers during COVID. Healthcare workers obviously came into their own too, but so many other workers were still taken for granted.
I visualize a person huffing when their internet is slow or intermittent with a guy out to sea working during a storm or under difficult conditions and I laugh at the juxtaposition and perspective of both. I also do rope work and had to resort to doing more of it during COVID because my 'desk work' dried up a bit. Hanging 300ft off of a building with a black balaclava and mask with all-black rigging equipment in NJ doing a facade inspection across from the FBI building was certainly a memorable one. (Note: all-black equipment is standard for theater and entertainment work to stay hidden. I did confirm the FBI building people were informed there would be 4 guys on ropes that day. You never know!). I have been programming since 1978, but I have always had to have some physicality to my work in order to be satisfied. I guess it's having a more tangible connection to the world not abstracted away several layers.
Interesting when Russia complains for decades not to have NATO encroach on their borders to the point where they invade Ukraine, but here the possibility a Chinese automaker is offered incentives from Mexico, the way they did for Tesla, is too much to handle for the US.
Either we can compete, or we can't. China can't subsidize for eternity without eventually failing, so why not take the short-term loss and pivot and win in the long-term? Also, Mexico would like to grow their economy as a sovereign nation too.
The article doesn't cover how this is concentrated locally (shoving incidents in the NYC subway - to the tracks) vs. state-wide, or how the 2 databases the Federal government maintains and uses, have been redefined, and with unreliable reporting by the states due to the lag in the new reporting format of the federal government, doesn't allow for a like comparison over previous datasets. I grew up in Sunset Park, Brooklyn during the late 60s, 70s, and 80s, and yes, homicides are down. I think it was around almost 3k per year for NY then, and is a factor of 10 less now. But we had things like Son of Sam, FALN bombings in NYC (49 of them in the 70s), hijackings at the NY airports (137 in the US alone in the 60s to 70s), etc...
Sure given the epicenter was in NJ and closer than Brooklyn. I am from Brooklyn, but live in Nyack, NY, and I felt it here. Nyack is 40mi from epicenter, Brooklyn ~60mi. But your experience could be different based on the structure you are in, floor elevation, and existing soil and ground conditions.
I wish the SEC would clean house of all the congress members and senators, Democrat and Republican, around 75 to 97 at last count, who had bought or sold stock or bonds, or other financial assets related to their congressional work. It's always the corporate boogeyman is always target number one in America. Pelosi and her ilk, including her husband, should have to live by the same laws as the people they supposedly represent.
Try April (Array Programming Reimagined In Lisp)[0] then. Sorry, I am both an array language and Lisp fan for many years. You use Lisp for all of its goodness, and drop into APL to do numerics and array work in a language better suited for the problem at hand.
Hmm, maybe a marriage between Gerbil and J -> Jerbil!
I've been a fan of Gambit for a long time too. Love to see it being utilized this way.
I don't usually read the Telegraph, but Macron just doubled down about "Western" boots on the ground, so I am all for any hesitancy to turn this into WWIII by sending "advisors". From my other comment, that is how Vietnam started for the US with 25,000 "advisors" there before the official first combat wave of 25,000 US Marines on 8 March 1965.
This is how it all starts. The US had 25,000 "advisors" on the ground in Vietnam before the official 8 March 1965 US Marine landings at Da Nang. I don't blame the Germans for being transparent, so the people know what we might be getting into here.
You will see posts about the aggregate number of French, UK, and German forces, which seems like it is enough without the US to have a shot at fighting Russia, but these are mainly troops with little experience in recent history of taking on a willing enemy. Given we have depleted our conventional weapons by supplying Israel and Ukraine, and that Russia is putting nuclear missiles on display on their streets, it should be time to go to the table before the battlefield. Ukraine released a 31,000 people killed figure that the West agrees is conservatively twice that, but reports from Ukraine and Ukrainian soldiers hint it is well above 150,000. This is why they are recruiting everyone they can by pulling them off the streets and out of buses and trains as long as they are under 65 at this point and can walk.