I've been successfully practicing programming with proof of correctness since the 1970s. The confusion I see with most people failing at this is that they're trying to write code first and then prove it correct. The idea promoted by Dijkstra, Hoare, et al is to write the code and the proof together, with each of these aspects of the task supporting the other. The result is (in my experience) a better program developed as quickly (even when not counting on vastly decreased debugging time) as pure coding. Similarly with strong lexical typing: One does not try to create a typing model for a hunk of arbitrary code. Instead, one develops the type model along with the code, with each of those aspects supporting the other. Putting it all together: Coding, Typing (and other Constraining) and Proving are done together, with each of these activities supporting the others. It does take time to learn such a methodology. And it takes extra understanding to maintain types, constraints and proofs as the program evolves, i.e. "maintenance".
HN user
GregDavidson
Emacs is a Platform. Operating Systems are also Platforms. Many other things are platforms. A platform is a layer of software designed to enable you to build new things on it. This should raise the question: What platform X would be good for building this thing Y I want to build? I often find X = Emacs, but also Racket, Rust, et al. An application which is also a good platform may be worth a greater learning investment than a simpler application would justify.
I use formal verification as part of my development process. The needs of the proof guide the development of the code as much as vice-versa. The result is usually cleaner, simpler, smaller and usually more efficient programs developed much faster as debugging effort is minimal. I still create complete test cases. Proof maintenance as code changes is a pain and I would like LLMs and/or other tools to help with that. I would never try to formally verify code written with regular processes!
I learned to read English the same way I learned to understand it spoken: exposure. As a young child a relative would put me in their lap and a book I liked in my lap and read to me. After awhile I was reading fluently without effort. Most schools teach reading as a conscious intellectual decoding task which leaves little brain power left to engage with the material - the same way most schools teach "foreign" languages. Engage the brain's language centers and language skills will be fluent.
I started with Fortran 2 which has subroutines which don't behave as black boxes. It took me months of frustrated study to understand procedure calls in decent languages as delegation. That opened up the world of high-level computing. Later I would teach this using problems that were a good fit for "recursion". Recursion is not a feature, it's just an obvious pattern of the more general and important nature of delegation. While recursion is occasionally a useful technique, it's tremendously valuable as a tool for learning how to think about procedures as black boxes!
Everything I run on servers I also run on my laptop. Occasionally I get crashes or corruption because of the lack of ECC memory. I'd also like to be able to swap parts between a modular laptop and a home/small-office server, but again - I want ECC. If framework had a model with ECC I'd be all in!
Regulatory systems need omsbuds within the government who can ask for help and explanations from all the agencies regulating a project yet are (primarily) accountable for helping projects succeed as soon as possible and (secondarily) responsible for providing transparent feedback to those agencies and the public where regulation is malfunctioning.
This technology is completely amazing - for large fleet vehicles like buses, trucks, ferries, etc. Also airplanes! Getting this so compact and refined is a technological miracle. Now put it where it fits!
Do what Linus does: Focus on code quality!
Culture is huge nested networks of memes[1] which reinforce themselves and evolve via natural selection. Their substrate is our brains. [1] https://en.wikipedia.org/wiki/Memetics
Only train when the Sun shines.
Realistic Hard SF has to deal with Accelerating Change making technology vastly powerful yet still limited. The hardest thing to write about is cognitively enhanced humans or any other entities (AI, aliens, etc.) exceeding human cognitive limits. JW Campbell famously said it couldn't be done, but without that depictions of the future or wider universe fall flat. Vernor Vinge became the master of such SF and showed several ways to do it. I recommend everything he wrote! Good Hard SF requires an author who has a good grasp of science without that stifling their imagination. It's easy if you cheat but Science Fantasy is unreadable by the science literate folks who frequent HN. Good Hard SF is out there, with and without spaceships, but you'll have to hunt for it - and thanks for all the recommendations here!
GTD in https://orgmode.org/
I'm a geek and have shared my home with housemates for 50 years. When I was poor and when I was prosperous. When I was married and when I was not. It's almost always been good for me, including for growth in my social intelligence. It was especially valuable when my wife died. Some of my housemates have been challenging. More became close friends. Living together people take their masks off. Quality social connections have been invaluable to me.
AI used to refer to the extensive range of techniques of the field of Artificial Intelligence. Now it refers to LLMs and maybe other multi-layer networks trained on vast datasets. LLMs are great for some tasks and are also great as parts of hybrid systems like the IBM Watson Jepardy system. There's much more to Artificial Intelligence, e.g. https://en.m.wikipedia.org/wiki/Knowledge_representation_and... et al.
I learned to read by being read to: typically on a relative's lap with the book in my lap. They were not trying to teach me how to read, but my language centers took care of the job, just like they did for spoken language, long before schools could muck it up. Reading has always been fast and effortless for me, requiring no conscious attention - again, just like spoken language. Much later I studied the linguistics of language, grammar, spelling systems, etc. which revealed the wonders of our natural language skills. I recommend the natural method for everyone. Be sure to check for eyesight problems, though.
Important quote! Citation?
My Twiddler comes from Winnipeg -- https://www.mytwiddler.com/
The biggest difference between now and the 1990s is in the reduction of abject poverty worldwide. Death and disability from food shortage was extremely common in many countries. A huge improvement in the 1990s over the 1980s is that I could own my own computer (I bought a Sun-2 with Solaris) instead of having everything I created owned by the institution which owned the computer I needed. Today's consumer products, though, are a mixed bag. As an example, I wish I could buy a microwave oven as good as my first one. It was larger, had a temperature probe that could be used instead of time and it used a small internal metal wheel to distribute the microwaves evenly throughout the oven instead of wasting space for the silly rotating platter.
When the UC sold the UCSD P-System the profiler and native code compiler were abandoned. With P-Code optimized for size and hot spots native compiled, small P-System programs ran comparably to programs fully compiled to native code and large programs ran thousands of times faster by reducing (usually eliminating) swapping and paging on those early memory-starved systems. I too migrated to Sun-2s but I purchased them myself. I'd learned the hard way that software developers need to own the means of their production!
The UCSD "Computer Scientists" were a small group of undergraduates working in Ken Bowles' lab. We were supposedly following Professor Bowles' directions but he was a fairly conservative physicist and we had lots of radical ideas - fortunately he was tolerant. The p-code was not just machine independent - by careful design it was approximately 1/4 the size of native code on those early 8 and 16-bit microprocessors, allowing us to effectively almost quadruple the amount of code we could fit in 64K - minus the interpreter which was 8K of machine code and minus another 8K on PDP-11s for I/O space. We would also use native code for hotspots without appreciably expanding code size. This key idea is what allowed us to have a high-level OS and development environment on those dinky machines when everyone else was compromising quality to get things to fit. Alas, CopyLeft had not yet been invented, the UC sold the P-System and we lost legal access to the code we'd written.
vis rocks!
The power languages of the late 1960s and 1970s were awesome! I loved APL, InterLisp, Snobol-3, Smalltalk and SETL. Turtle Graphics with a robot turtle. Writing graphics for the Evans & Sutherland Picture System was awesome. Instead of C or Java we could build anything UCSD Pascal. But look around and you'll find all of these and more available now. Just ignore the blub languages and platforms!
A Gnu/Linux phone with Android in a container using WayDroid or AnBox gives you the best of both worlds.
I regularly use my Twiddler with my Android phone. It allows me to fully operate all the applications I use on my desktop computer, e.g. Emacs. https://www.mytwiddler.com/
Different oils vary a lot in how inflammatory they are. In addition, heating during extraction and/or aging or storage conditions can lead to cross linking which makes oils very bad for health. With the exception of olive oil's virgin labeling, I'm not aware of any easy way to navigate this health minefield.
You just got a convert! Huge value in sh compatibility. Bash, not so much!
bash, ksh, zsh and a few other shells have the awesome feature that if you call them with a link named "sh" they accept Posix Bourne-shell syntax.
This means you can make them your /bin/sh system shell which will be used to log you in and your login scripts can then set environment variables for your whole session. This feature is something I count on.
Some system shells (not dash) also allow login scripts to export essential shell functions to the session environment.
I would love to use a nicer shell, fish, oilsh, rc, etc. but it's gotta provide this key Posix compatibility. The Posix Bourne shell language is pretty simple. This is not a big ask.
I didn't connect miniKanren to Scheme. I said "Host Language." I did suggest the value of a multi-paradigm host language.
Oops: s/visible/viable/
Hydrogen fuel cells make more sense for aircraft (weight) and larger vehicles like trucks because of scaling (larger tanks are more efficient, etc.) and fleet advantages (depot refueling). It is amazing to me that Toyota has gotten hydrogen to work in cars, but it can't compete with batteries.