SoylentNews is people
SoylentNews
QuantaMagazine.org has a very long and interesting article on computers redefining the roots of Math.
On a recent train trip from Lyon to Paris, Vladimir Voevodsky sat next to Steve Awodey and tried to convince him to change the way he does mathematics.
Voevodsky, 48, is a permanent faculty member at the Institute for Advanced Study (IAS) in Princeton, N.J. He was born in Moscow but speaks nearly flawless English, and he has the confident bearing of someone who has no need to prove himself to anyone. In 2002 he won the Fields Medal, which is often considered the most prestigious award in mathematics.
[...] The idea of doing mathematics in a program like Coq has a long history. The appeal is simple: Rather than relying on fallible human beings to check proofs, you can turn the job over to computers, which can tell whether a proof is correct with complete certainty. Despite this advantage, computer proof assistants haven't been widely adopted in mainstream mathematics. This is partly because translating everyday math into terms a computer can understand is cumbersome and, in the eyes of many mathematicians, not worth the effort.
For nearly a decade, Voevodsky has been advocating the virtues of computer proof assistants and developing univalent foundations in order to bring the languages of mathematics and computer programming closer together. As he sees it, the move to computer formalization is necessary because some branches of mathematics have become too abstract to be reliably checked by people.
"The world of mathematics is becoming very large, the complexity of mathematics is becoming very high, and there is a danger of an accumulation of mistakes," Voevodsky said. Proofs rely on other proofs; if one contains a flaw, all others that rely on it will share the error.
This is something Voevodsky has learned through personal experience. In 1999 he discovered an error in a paper he had written seven years earlier. Voevodsky eventually found a way to salvage the result, but in an article last summer in the IAS newsletter, he wrote that the experience scared him. He began to worry that unless he formalized his work on the computer, he wouldn't have complete confidence that it was correct.
But taking that step required him to rethink the very basics of mathematics. The accepted foundation of mathematics is set theory. Like any foundational system, set theory provides a collection of basic concepts and rules, which can be used to construct the rest of mathematics. Set theory has sufficed as a foundation for more than a century, but it can't readily be translated into a form that computers can use to check proofs. So with his decision to start formalizing mathematics on the computer, Voevodsky set in motion a process of discovery that ultimately led to something far more ambitious: a recasting of the underpinnings of mathematics.
Geometry and classic algebra are not really isomorphic. Boolean logic and number theory were proved incompatible by Bertrand Russell
(Score: 2, Insightful) by Anonymous Coward on Wednesday October 04 2017, @03:48PM (32 children)
People think they are more productive with a dynamically typed language, but they're just being lazy: They are refusing to codify their abstractions in a way that a computer can check them, and then just waiting for catastrophe to occur at runtime.
Folks, what are computers for if not to do these kinds of calculations? Take pride in codifying your thoughts explicitly!
(Score: 1, Insightful) by Anonymous Coward on Wednesday October 04 2017, @03:58PM (17 children)
Some programming jobs are small enough that convenience of quick iteration and simple syntax beat the added reliability of type-checking.
(Score: 5, Insightful) by Anonymous Coward on Wednesday October 04 2017, @04:11PM (16 children)
More of than not, the slapdash prototype becomes the working production code. The more code I read, the more I realize that the entire planet runs on the cyber equivalent of chewing gum and duct tape. Your little shell script will become a fundamental component of your system. It WILL.
The only way to achieve large-scale excellence is to commit to such excellence even in the seemingly "unimportant" parts; it seems like a waste of time at first, but it's an investment that pays dividends in the long-run.
(Score: 0) by Anonymous Coward on Wednesday October 04 2017, @04:27PM (9 children)
And this is why you actually see deployment code that reads
wget -O - example.com/some.sh | bash -
(Score: 3, Insightful) by Runaway1956 on Wednesday October 04 2017, @05:08PM (8 children)
I'm not even a coder, but that hurts to even think about. Almost the equivalent of listening to an engine run without any oil, for awhile . . .
(Score: 1, Touché) by Anonymous Coward on Wednesday October 04 2017, @07:09PM
Come on, SoylentNews. Come on.
(Score: 2) by Pino P on Wednesday October 04 2017, @08:57PM (6 children)
When you wget or curl into bash, you're no more vulnerable than (say) when you install a package from a repository listed in your OS distribution's package manager. Or is the problem that there is no https: scheme on that wget command?
(Score: 0) by Anonymous Coward on Wednesday October 04 2017, @09:24PM (3 children)
That's not a rebuttal; that's just more proof that all of the computing world is built on a very poor foundation.
However, at least such repositories are increasingly using security concepts such as cryptographic webs of trust.
We can do so much better. We have the technology.
(Score: 2) by Pino P on Thursday October 05 2017, @02:37PM (2 children)
I'm confused as to how a web of trust can become dense enough to provide reasonable faith in someone's identity if there aren't enough people who travel internationally to key signing parties. International tourism is expensive, as are specialist legal services to determine whether key signing constitutes prohibited "work" on a tourist visa. Besides, even if you do get to a key signing party, vouching for someone's identity doesn't necessarily imply vouching for that person's ability to validate others' identities.
(Score: 0) by Anonymous Coward on Friday October 06 2017, @12:25AM (1 child)
You don't have to meet people face-to-face to build such a web-of-trust; it is enough to publish a public key widely (e.g., across a sufficient number of independent sources) so that an attacker couldn't practically fake it.
(Score: 2) by Pino P on Tuesday October 10 2017, @08:18PM
What prevents an attacker from publishing a key widely before you do?
(Score: 2) by coolgopher on Thursday October 05 2017, @01:19AM (1 child)
No, clearly the problem is that it was piping into a regular bash, not a sudo'd bash for guaranteed root access! ;)
(Score: 2) by Pino P on Thursday October 05 2017, @02:26PM
You don't usually need administrative privilege to install executables to your user account.
(Score: 0) by Anonymous Coward on Wednesday October 04 2017, @04:46PM (5 children)
If your code has a lot of calculation, you can use MATLAB/Octave and easily build on well-established built-in functions. Or you can use GSL with C/C++, which has a much steeper learning curve, and will never read as cleanly. As the saying goes, the perfect is the enemy of the good.
(Score: 0) by Anonymous Coward on Wednesday October 04 2017, @05:39PM (3 children)
Try again.
(Score: 0) by Anonymous Coward on Wednesday October 04 2017, @09:26PM (2 children)
The whole point of that saying is to highlight that there is a real dichotomy between the perfect and the good. While the set of perfect things may be included in the set of good things, in many situations the perfect set is the empty set, and to insist on perfection is to discount everything in the good set.
(Score: 0) by Anonymous Coward on Wednesday October 04 2017, @10:02PM (1 child)
In your world, the set of perfect things is often empty because you've bungled the foundations on which your solutions are built. Start over, and take perfection a little more seriously this time.
(Score: 0) by Anonymous Coward on Friday October 06 2017, @02:57PM
If you think everything you do is perfect, I don't think the GP is the one that needs to come to reality.
(Score: 1) by ewk on Thursday October 05 2017, @08:13AM
"well-established built-in functions"
But, without actual proof that these WEBIFs are correct, you're still (theorically) building on quicksand.
Curious: Does MATLAB or Octave with such a formal proof of correctness?
I don't always react, but when I do, I do it on SoylentNews
(Score: 3, Insightful) by Anonymous Coward on Wednesday October 04 2017, @07:01PM (3 children)
This is not only true, but it explains the absurd state of security of the web. You can actually name the root of nearly every web exploit, hack, bug, and everything with one word: javascript. It was built decades ago and never meant to be used in anything like the way it is today. As a random example, do people ever consider how absurd it is that jquery is non-native? Or speaking of jquery, go take trace the most basic call using it... That's the stuff nightmares are made of. This isn't a language evolving. This is people taking some old wood collected to build a tool shed with, and trying to build sky scrapers out of it. Each time it, completely unexpectedly.., comes crashing down - no problem, it just needs a bit more glue there next time.
Some individuals take it almost as a sort of pride that anything you learn (in this domain) will be obsolete in a few years. That's true. It's also completely idiotic. It's indicative more than anything else not of evolution, but of an indicator that the tool being used is simply inappropriate for what it's being used for. And while I pick on javascript this is true of the entire base of the web. A [mostly] single page, dynamically driven, secure website with a stateful connection, is what 99% of users want. But the tools we're using to make these things were simply not designed for that. It's all obsolete, and in desperate needs of a reboot.
(Score: 2) by crafoo on Wednesday October 04 2017, @08:51PM (2 children)
javascript was a mistake.
running code in the browser was, and continues to be a mistake.
(Score: 2) by Pino P on Wednesday October 04 2017, @09:00PM
What means of deploying an application to multiple operating systems isn't a mistake?
(Score: 0) by Anonymous Coward on Thursday October 05 2017, @07:33PM
PHB's and consumers will almost always choose eye-candy and fads over security, unless the security risks are made very clear to them and they don't have to trust you to believe it.
(Score: 1) by rylyeh on Wednesday October 04 2017, @09:47PM (1 child)
I like to use the right tool (typed or dynamic) for the task.
That's why there are numerous languages that have different type systems.
Saying 'All dynamically typed stuff is sh*t' is not quite fair.
Code that will be consumed in a library that is itself consumed for an API? Strong typing might be indicated.
A script that runs as a watchdog? Dynamic typing might be the best.
Shouldn't the form fit the function?
I have also found that many of the 'type' decisions made for which language to use are about time, reliability, audience and cost.
"a vast crenulate shell wherein rode the grey and awful form of primal Nodens, Lord of the Great Abyss."
(Score: 0) by Anonymous Coward on Wednesday October 04 2017, @10:08PM
Here, I'll do it for you: The right tool is the one that allows the computer to analyze the correctness of the code as much as possible before run-time.
(Score: 2) by shortscreen on Thursday October 05 2017, @01:35AM (2 children)
The idea of types is itself an abstraction. In reality there is only one type: binary. That's what the computer deals with. The only difference between these bits and those bits is how they are interpreted. Humans have to decide how the bits should be interpreted. But that would require them to think about data structures which they are mostly too lazy to do. Anyway, what I'm trying to say here is that types are baloney. And so are programming languages. I'll take NASM instead any day.
(Score: 1) by rylyeh on Thursday October 05 2017, @03:27AM
Yes! I had to use LISA on an Apple II. Worked great! Better than trying to type the opcodes and data by hand in the mini-assembler!
"a vast crenulate shell wherein rode the grey and awful form of primal Nodens, Lord of the Great Abyss."
(Score: 2) by maxwell demon on Thursday October 05 2017, @07:46AM
NASM? How dare you. The most of a tool you should use is xxd! :-)
The Tao of math: The numbers you can count are not the real numbers.
(Score: 3, Informative) by TheRaven on Thursday October 05 2017, @10:24AM (4 children)
Assuming that you're not trolling, allow me to give you a counterpoint:
Type theory is one way of encoding constraints. Most mainstream programming languages have restrictive type systems that don't allow you to encode various things that are generally useful. In a fully dynamically typed language, you use explicit assertions (for example: must implement this protocol, must provide this method) that are checked at run time, but these are generally the least useful checks: if you're making errors related to the sorts of things that most mainstream programming languages can check then you have problems. Here's a trivial example: In your favourite statically typed language, how do you express in the type system that a sort function is correct (i.e. that, for all inputs, the output will have the same set of elements as the input and that they will respect the specified partial ordering)? That's a trivial correctness property in comparison to most programs, yet one that is beyond the scope of most static type systems.
At the opposite extreme are languages with Turing-complete type systems. There are quite a few of these, though C++ is the only one that's made it into the mainstream. You can, using C++ templates (or, in C++11 or later, templates and constexpr functions, and ideally templates in combination with static assertions), check any arbitrary property of your program that can be known at compile time. This is hugely powerful, but it has a serious limitation: type checking the program reduces to the halting problem. I am currently working on a research project that takes around 2 minutes for template instantiation on a single (fairly small) compilation unit because it is performing a huge number of static checks that go far beyond anything that most other mainstream statically typed languages can do (and, as a result, catches a lot of subtle bugs at compile time). Unfortunately, sometimes when I make an error in this code the compile time jumps to 10+ minutes. Sometimes, when I make a correct change, it fails to compile with a confusing error. The reason for both of these is that the compiler has limits (configurable by command-line flag) for recursion depth of template instantiation and constexpr function invocations. When a check involving a constexpr function fails to terminate in the bounded number of invocations, the error message tells me that a value is not a constant (which is confusing, because the value is a constant, it's just that the compiler gave up trying to evaluate it too early).
It is provably impossible to determine whether an arbitrary string is a valid C++ program for precisely this reason: the results of constexpr evaluations and template instantiations can perform any arbitrary computation and so you have to solve the halting problem to tell whether it's actually wrong or whether it's just taking a really long time.
If you really care about correctness, then you shouldn't use a language that tries to shoehorn arbitrary checks into a type system, you should use a language that's designed explicitly for proof-carrying code. F* is the closest example that I'm aware of to being a mainstream language: It's a variant of F# that uses the Z3 SMT solver to check correctness proofs written in the same language as the rest of the program. Unfortunately, it suffers from the same problem: sometimes, correct proofs will time out in the solver, so you can only compile a subset of all correct programs.
TL;DR: There's no silver bullet. Trivial type systems will catch trivial errors, complex type systems may never terminate checking correct programs.
sudo mod me up
(Score: 0) by Anonymous Coward on Friday October 06 2017, @12:29AM (1 child)
Why is everything today labeled "Trolling"? I just... I don't even know what that means anymore.
(Score: 2) by TheRaven on Friday October 06 2017, @11:02AM
sudo mod me up
(Score: 0) by Anonymous Coward on Friday October 06 2017, @12:36AM (1 child)
What's wrong with reporting to the user that a program (or fragment thereof) is correct with a probably 80% or whatever? Then, build-time policy can be set: Failure is when probability is less 95%, and we know we have to increase build-time computing resources until the compiler reaches this level of truth.
(Score: 2) by TheRaven on Friday October 06 2017, @11:05AM
sudo mod me up