https://yairchu.github.io/glog/
I built glog for myself and other humans who still read code and use Git while coding agents do more of the writing.In other Git TUIs, my muscle memory from `git log` and `git show` accidentally triggered destructive rebases. glog is strictly read-only, so I can browse without worry.It shows commits with syntax highlighting via delta, uses familiar pager keys, and has opinionated,...
IIUC a regular programming language with a certain set of restrictions already duals as a proof-assistant as discovered by Curry & Howard. By restrictions, I mean something like how Rust forces you to follow certain rules compared to Java.
(regarding ANA's "More than 50 years ago, the FDA approved a drug. Today, we’re evaluating that drug as a treatment for COVID-19")
Is that so?!
I’m an Israeli and I assumed that it’s the really bad education that is responsible for stronger skepticism and Chutzpah.
A huge benefit of text is that if you learn to read code, you already know how to edit it too. This is because of WYTIWYS: What you type is what you see.
Higher level edits and refactoring are awesome, but when you just start using the environment you can't learn all the refactorings yet, while you only want to enter something similar to the code you saw on the whiteboard in class etc. WYTIWYS makes it easy.
Historically, many attempts at structural or projectional editors didn't adhere to WYTIWYS. I believe that this is a major reason for why they haven't gained popularity.
But recently there are several projects developing projectional editors which do adhere to WYTIWYS!
One is Lamdu (http://www.lamdu.org) (btw I'm one of its developers). In Lamdu we try to create a programming language with a friendly projectional editor which does adhere to WYTIWYS and also offers awesome unique features that projectional editors enable. (for more information see our short videos - https://www.youtube.com/channel/UCgvPEOFglvS4_ZEHi-PEctQ )
Another projectional editor adhering to WYTIWYS is Jetbrains MPS (https://www.jetbrains.com/mps/) . This one isn't limited to a single programming language! It is a general purpose language workbench.
There's the "Stream" nominal type, shown below in Haskell-like text syntax:
newtype Stream a = () -> (Empty | NonEmpty { head :: a, tail :: Stream a })
Now the type of the value inside the hole within is just "Empty | NonEmpty { head :: a, tail :: Stream a }", now type "nonempty" and pick it.
Here's an explanation of what the term means: http://blog.absentdesign.com/2013/05/blindly-manipulating-sy...
Note that not seen in the screenshot are the `reduce` and `max` functions which I've implemented, though those are pretty simple.
I also can't wait till I'll be able to really use Lamdu.
It's been clear to us that we need animations for structural editing so that it's clear to the user what's going on, and we're not familiar with a GUI library that provides us with what we needed, so we made this custom one.
Currently it's part of Lamdu's sources, but we could make it an independent library if there's demand.
Indeed the fonts may not be as pretty as with Cairo etc but on the other hand there are very nice animations when edits make stuff move around.
The problem with cheap AI and robots is not that people will not want to create things for each other and do stuff - sure they will still want to make stuff.
The problem is that hardly anyone will pay them for doing stuff, and therefore it will be impossible for them to make a living. So, the non-rich people (who don't own the robot corporations) would not be able to afford food and shelter.. (and they'll die as a consequence)
Unless government or benevolent fellows decide to help the destitute population and provide for them, which I don't really see happening as the plutocrats would probably treat the poor just like white slave owners in the US used to treat their black slaves, or like people treat cows. Even though resources will be abundant and it won't take much effort or sacrifice to help us, they would rather spend their resources on building faster spaceships or go ride space slides or ski on Mars or something.
Two years ago when Mubarak told the Egyptian army to spray protestors with bullets, and the soldiers refused. That's because he didn't have a robotic force. The future is probably going to be horrible.
Cubic equations were researched by mathematicians for thousands of years before Tartaglia solved the general case! (btw the solution for Quadratic equations was well known since at least 2000 BC)
And he also made up the complex numbers on the way!
Wrt whether he was an outsider, http://en.wikipedia.org/wiki/Niccol%C3%B2_Fontana_Tartaglia
> There is a story that Tartaglia learned only half the alphabet from a private tutor before funds ran out, and he had to learn the rest for himself. Be that as it may, he was essentially self-taught. He and his contemporaries, working outside the academies, were responsible for the spread of classic works in modern languages among the educated middle class.
After Tartaglia's solution for Cubic equations and Ferrari's solution for Quartic equations were published in 1545, no doubt that finding a solution for 5th degree polynomials became a hot topic. http://en.wikipedia.org/wiki/Quintic_function
> Finding the roots of a given polynomial has been a prominent mathematical problem.
But even though it was a hot topic, it took 300 years until Galois came around with a method to determine which Quintic equations can and which cannot be factored to "radicals".
In this case, it is simply the post title being misleading, as it's not the Nobel prize these folks won, but the Nobel memorial prize in economics, which is a relatively new prize which is not part of the 5 Nobel prizes which had been given by Nobel's estate for more than a century.
Edit: oh I see they didn't reward a dead in this case, misread your comment..
I don't know Javascript so I may be wrong here, but:
* Suppose someone uses this library to create a "MariaSQL Explorer App", where you give the app connection credentials and it connects to the database and shows you the data etc.
* A malicious attacker tells a user "have a look at my database" and the user goes to the attacker's database.
* The attacker's database (or spoof of one) has a column called 'dummy": MALICIOUS_CODE(), "colname'. notice the '"' chars inside column name.
* The MALICIOUS_CODE() runs in the user's node.js app. Perhaps it sends the attacker the passwords to other databases from the app's keychain or something..
* Profit