nhaliday + heavyweights + reflection   21

The Future of Mathematics? [video] | Hacker News
https://news.ycombinator.com/item?id=20909404
Kevin Buzzard (the Lean guy)

- general reflection on proof asssistants/theorem provers
- Kevin Hale's formal abstracts project, etc
- thinks of available theorem provers, Lean is "[the only one currently available that may be capable of formalizing all of mathematics eventually]" (goes into more detail right at he end)
hn  commentary  discussion  video  talks  presentation  math  formal-methods  expert-experience  msr  frontier  state-of-art  proofs  rigor  education  higher-ed  optimism  prediction  lens  search  meta:research  speculation  exocortex  skunkworks  automation  research  math.NT  big-surf  software  parsimony  cost-benefit  intricacy  correctness  programming  pls  python  functional  haskell  heavyweights  research-program  review  reflection  multi  pdf  slides  oly  experiment  span-cover  git  vcs  teaching  impetus  academia  composition-decomposition  coupling-cohesion  database  trust  types  plt  lifts-projections  induction  critique  beauty  truth  elegance  aesthetics 
8 days ago by nhaliday
One week of bugs
If I had to guess, I'd say I probably work around hundreds of bugs in an average week, and thousands in a bad week. It's not unusual for me to run into a hundred new bugs in a single week. But I often get skepticism when I mention that I run into multiple new (to me) bugs per day, and that this is inevitable if we don't change how we write tests. Well, here's a log of one week of bugs, limited to bugs that were new to me that week. After a brief description of the bugs, I'll talk about what we can do to improve the situation. The obvious answer to spend more effort on testing, but everyone already knows we should do that and no one does it. That doesn't mean it's hopeless, though.

...

Here's where I'm supposed to write an appeal to take testing more seriously and put real effort into it. But we all know that's not going to work. It would take 90k LOC of tests to get Julia to be as well tested as a poorly tested prototype (falsely assuming linear complexity in size). That's two person-years of work, not even including time to debug and fix bugs (which probably brings it closer to four of five years). Who's going to do that? No one. Writing tests is like writing documentation. Everyone already knows you should do it. Telling people they should do it adds zero information1.

Given that people aren't going to put any effort into testing, what's the best way to do it?

Property-based testing. Generative testing. Random testing. Concolic Testing (which was done long before the term was coined). Static analysis. Fuzzing. Statistical bug finding. There are lots of options. Some of them are actually the same thing because the terminology we use is inconsistent and buggy. I'm going to arbitrarily pick one to talk about, but they're all worth looking into.

...

There are a lot of great resources out there, but if you're just getting started, I found this description of types of fuzzers to be one of those most helpful (and simplest) things I've read.

John Regehr has a udacity course on software testing. I haven't worked through it yet (Pablo Torres just pointed to it), but given the quality of Dr. Regehr's writing, I expect the course to be good.

For more on my perspective on testing, there's this.

Everything's broken and nobody's upset: https://www.hanselman.com/blog/EverythingsBrokenAndNobodysUpset.aspx
https://news.ycombinator.com/item?id=4531549

https://hypothesis.works/articles/the-purpose-of-hypothesis/
From the perspective of a user, the purpose of Hypothesis is to make it easier for you to write better tests.

From my perspective as the primary author, that is of course also a purpose of Hypothesis. I write a lot of code, it needs testing, and the idea of trying to do that without Hypothesis has become nearly unthinkable.

But, on a large scale, the true purpose of Hypothesis is to drag the world kicking and screaming into a new and terrifying age of high quality software.

Software is everywhere. We have built a civilization on it, and it’s only getting more prevalent as more services move online and embedded and “internet of things” devices become cheaper and more common.

Software is also terrible. It’s buggy, it’s insecure, and it’s rarely well thought out.

This combination is clearly a recipe for disaster.

The state of software testing is even worse. It’s uncontroversial at this point that you should be testing your code, but it’s a rare codebase whose authors could honestly claim that they feel its testing is sufficient.

Much of the problem here is that it’s too hard to write good tests. Tests take up a vast quantity of development time, but they mostly just laboriously encode exactly the same assumptions and fallacies that the authors had when they wrote the code, so they miss exactly the same bugs that you missed when they wrote the code.

Preventing the Collapse of Civilization [video]: https://news.ycombinator.com/item?id=19945452
- Jonathan Blow

NB: DevGAMM is a game industry conference

- loss of technological knowledge (Antikythera mechanism, aqueducts, etc.)
- hardware driving most gains, not software
- software's actually less robust, often poorly designed and overengineered these days
- *list of bugs he's encountered recently*:
https://youtu.be/pW-SOdj4Kkk?t=1387
- knowledge of trivia becomes more than general, deep knowledge
- does at least acknowledge value of DRY, reusing code, abstraction saving dev time
techtariat  dan-luu  tech  software  error  list  debugging  linux  github  robust  checking  oss  troll  lol  aphorism  webapp  email  google  facebook  games  julia  pls  compilers  communication  mooc  browser  rust  programming  engineering  random  jargon  formal-methods  expert-experience  prof  c(pp)  course  correctness  hn  commentary  video  presentation  carmack  pragmatic  contrarianism  pessimism  sv  unix  rhetoric  critique  worrydream  hardware  performance  trends  multiplicative  roots  impact  comparison  history  iron-age  the-classics  mediterranean  conquest-empire  gibbon  technology  the-world-is-just-atoms  flux-stasis  increase-decrease  graphics  hmm  idk  systems  os  abstraction  intricacy  worse-is-better/the-right-thing  build-packaging  microsoft  osx  apple  reflection  assembly  things  knowledge  detail-architecture  thick-thin  trivia  info-dynamics  caching  frameworks  generalization  systematic-ad-hoc  universalism-particularism  analytical-holistic  structure  tainter  libraries  tradeoffs  prepping  threat-modeling  network-structure  writing  risk  local-glob 
may 2019 by nhaliday
soft question - Thinking and Explaining - MathOverflow
- good question from Bill Thurston
- great answers by Terry Tao, fedja, Minhyong Kim, gowers, etc.

Terry Tao:
- symmetry as blurring/vibrating/wobbling, scale invariance
- anthropomorphization, adversarial perspective for estimates/inequalities/quantifiers, spending/economy

fedja walks through his though-process from another answer

Minhyong Kim: anthropology of mathematical philosophizing

Per Vognsen: normality as isotropy
comment: conjugate subgroup gHg^-1 ~ "H but somewhere else in G"

gowers: hidden things in basic mathematics/arithmetic
comment by Ryan Budney: x sin(x) via x -> (x, sin(x)), (x, y) -> xy
I kinda get what he's talking about but needed to use Mathematica to get the initial visualization down.
To remind myself later:
- xy can be easily visualized by juxtaposing the two parabolae x^2 and -x^2 diagonally
- x sin(x) can be visualized along that surface by moving your finger along the line (x, 0) but adding some oscillations in y direction according to sin(x)
q-n-a  soft-question  big-list  intuition  communication  teaching  math  thinking  writing  thurston  lens  overflow  synthesis  hi-order-bits  👳  insight  meta:math  clarity  nibble  giants  cartoons  gowers  mathtariat  better-explained  stories  the-trenches  problem-solving  homogeneity  symmetry  fedja  examples  philosophy  big-picture  vague  isotropy  reflection  spatial  ground-up  visual-understanding  polynomials  dimensionality  math.GR  worrydream  scholar  🎓  neurons  metabuch  yoga  retrofit  mental-math  metameta  wisdom  wordlessness  oscillation  operational  adversarial  quantifiers-sums  exposition  explanation  tricki  concrete  s:***  manifolds  invariance  dynamical  info-dynamics  cool  direction  elegance  heavyweights  analysis  guessing  grokkability-clarity  technical-writing 
january 2017 by nhaliday
The capacity to be alone | Quomodocumque
In fact, most of these comrades who I gauged to be more brilliant than I have gone on to become distinguished mathematicians. Still from the perspective or thirty or thirty five years, I can state that their imprint upon the mathematics of our time has not been very profound. They’ve done all things, often beautiful things in a context that was already set out before them, which they had no inclination to disturb. Without being aware of it, they’ve remained prisoners of those invisible and despotic circles which delimit the universe of a certain milieu in a given era. To have broken these bounds they would have to rediscover in themselves that capability which was their birthright, as it was mine: The capacity to be alone.
math  reflection  quotes  scholar  mathtariat  lens  optimate  serene  individualism-collectivism  the-monster  humility  the-trenches  virtu  courage  emotion  extra-introversion  allodium  ascetic  heavyweights  psychiatry 
september 2016 by nhaliday
soft question - How do you not forget old math? - MathOverflow
Terry Tao:
I find that blogging about material that I would otherwise forget eventually is extremely valuable in this regard. (I end up consulting my own blog posts on a regular basis.) EDIT: and now I remember I already wrote on this topic: terrytao.wordpress.com/career-advice/write-down-what-youve-d‌​one

fedja:
The only way to cope with this loss of memory I know is to do some reading on systematic basis. Of course, if you read one paper in algebraic geometry (or whatever else) a month (or even two months), you may not remember the exact content of all of them by the end of the year but, since all mathematicians in one field use pretty much the same tricks and draw from pretty much the same general knowledge, you'll keep the core things in your memory no matter what you read (provided it is not patented junk, of course) and this is about as much as you can hope for.

Relating abstract things to "real life stuff" (and vice versa) is automatic when you work as a mathematician. For me, the proof of the Chacon-Ornstein ergodic theorem is just a sandpile moving over a pit with the sand falling down after every shift. I often tell my students that every individual term in the sequence doesn't matter at all for the limit but somehow together they determine it like no individual human is of any real importance while together they keep this civilization running, etc. No special effort is needed here and, moreover, if the analogy is not natural but contrived, it'll not be helpful or memorable. The standard mnemonic techniques are pretty useless in math. IMHO (the famous "foil" rule for the multiplication of sums of two terms is inferior to the natural "pair each term in the first sum with each term in the second sum" and to the picture of a rectangle tiled with smaller rectangles, though, of course, the foil rule sounds way more sexy).

One thing that I don't think the other respondents have emphasized enough is that you should work on prioritizing what you choose to study and remember.

Timothy Chow:
As others have said, forgetting lots of stuff is inevitable. But there are ways you can mitigate the damage of this information loss. I find that a useful technique is to try to organize your knowledge hierarchically. Start by coming up with a big picture, and make sure you understand and remember that picture thoroughly. Then drill down to the next level of detail, and work on remembering that. For example, if I were trying to remember everything in a particular book, I might start by memorizing the table of contents, and then I'd work on remembering the theorem statements, and then finally the proofs. (Don't take this illustration too literally; it's better to come up with your own conceptual hierarchy than to slavishly follow the formal hierarchy of a published text. But I do think that a hierarchical approach is valuable.)

Organizing your knowledge like this helps you prioritize. You can then consciously decide that certain large swaths of knowledge are not worth your time at the moment, and just keep a "stub" in memory to remind you that that body of knowledge exists, should you ever need to dive into it. In areas of higher priority, you can plunge more deeply. By making sure you thoroughly internalize the top levels of the hierarchy, you reduce the risk of losing sight of entire areas of important knowledge. Generally it's less catastrophic to forget the details than to forget about a whole region of the big picture, because you can often revisit the details as long as you know what details you need to dig up. (This is fortunate since the details are the most memory-intensive.)

Having a hierarchy also helps you accrue new knowledge. Often when you encounter something new, you can relate it to something you already know, and file it in the same branch of your mental tree.
thinking  math  growth  advice  expert  q-n-a  🎓  long-term  tradeoffs  scholar  overflow  soft-question  gowers  mathtariat  ground-up  hi-order-bits  intuition  synthesis  visual-understanding  decision-making  scholar-pack  cartoons  lens  big-picture  ergodic  nibble  zooming  trees  fedja  reflection  retention  meta:research  wisdom  skeleton  practice  prioritizing  concrete  s:***  info-dynamics  knowledge  studying  the-trenches  chart  expert-experience  quixotic  elegance  heavyweights 
june 2016 by nhaliday
Answer to What is it like to understand advanced mathematics? - Quora
thinking like a mathematician

some of the points:
- small # of tricks (echoes Rota)
- web of concepts and modularization (zooming out) allow quick reasoning
- comfort w/ ambiguity and lack of understanding, study high-dimensional objects via projections
- above is essential for research (and often what distinguishes research mathematicians from people who were good at math, or majored in math)
math  reflection  thinking  intuition  expert  synthesis  wormholes  insight  q-n-a  🎓  metabuch  tricks  scholar  problem-solving  aphorism  instinct  heuristic  lens  qra  soft-question  curiosity  meta:math  ground-up  cartoons  analytical-holistic  lifts-projections  hi-order-bits  scholar-pack  nibble  the-trenches  innovation  novelty  zooming  tricki  virtu  humility  metameta  wisdom  abstraction  skeleton  s:***  knowledge  expert-experience  elegance  judgement  advanced  heavyweights  guessing 
may 2016 by nhaliday
Work hard | What's new
Similarly, to be a “professional” mathematician, you need to not only work on your research problem(s), but you should also constantly be working on learning new proofs and techniques, going over important proofs and papers time and again until you’ve mastered them. Don’t stay in your mathematical comfort zone, but expand your horizon by also reading (relevant) papers that are not at the heart of your own field. You should go to seminars to stay current and to challenge yourself to understand math in real time. And so on. All of these elements have to find their way into your daily work routine, because if you neglect any of them it will ultimately affect your research output negatively.
- from the comments
advice  academia  math  reflection  career  expert  gowers  long-term  🎓  aphorism  grad-school  phd  scholar  mathtariat  discipline  curiosity  🦉  nibble  org:bleg  the-trenches  meta:research  gtd  stamina  vitality  s:**  info-dynamics  expert-experience  heavyweights 
april 2016 by nhaliday

bundles : meta

related tags

:)  abstraction  academia  advanced  adversarial  advice  aesthetics  algebra  allodium  analogy  analysis  analytical-holistic  anglo  aphorism  apple  applications  art  ascetic  assembly  automation  beauty  berkeley  better-explained  big-list  big-picture  big-surf  books  britain  browser  build-packaging  c(pp)  caching  career  carmack  cartoons  characterization  chart  checking  checklists  civilization  clarity  classic  commentary  communication  comparison  compilers  complex-systems  composition-decomposition  computation  concrete  conquest-empire  contrarianism  cool  correctness  cost-benefit  coupling-cohesion  courage  course  cracker-prog  creative  critique  cs  curiosity  dan-luu  darwinian  database  dataviz  debugging  decision-making  design  desktop  detail-architecture  dimensionality  diogenes  direction  discipline  discussion  dynamical  early-modern  education  elegance  email  emotion  engineering  ergodic  error  essay  examples  exocortex  experiment  expert  expert-experience  explanans  explanation  exposition  extra-introversion  extrema  facebook  fedja  flux-stasis  form-design  formal-methods  frameworks  frontier  functional  games  generalization  geometry  giants  gibbon  git  github  google  gowers  grad-school  graphics  grokkability  grokkability-clarity  ground-up  growth  gtd  guessing  guide  gwern  hardware  haskell  heavyweights  heuristic  hi-order-bits  high-variance  higher-ed  history  hmm  hn  homogeneity  humility  ideas  idk  impact  impetus  increase-decrease  individualism-collectivism  induction  inference  info-dynamics  info-foraging  innovation  insight  instinct  interdisciplinary  intricacy  intuition  invariance  iron-age  isotropy  iteration-recursion  jargon  judgement  julia  knowledge  latex  learning  lens  letters  libraries  lifts-projections  linear-algebra  links  linux  list  local-global  logic  lol  long-term  manifolds  math  math.CA  math.CT  math.GN  math.GR  math.NT  mathtariat  meaningness  mediterranean  mental-math  meta:math  meta:reading  meta:research  metabuch  metal-to-virtual  metameta  methodology  microsoft  moments  mooc  motivation  move-fast-(and-break-things)  msr  multi  multiplicative  narrative  network-structure  neurons  nibble  notation  novelty  old-anglo  oly  operational  optimate  optimism  org:bleg  org:edu  org:junk  org:mat  os  oscillation  oss  osx  overflow  p:null  p:someday  p:whenever  papadimitriou  papers  parsimony  pdf  performance  pessimism  phd  philosophy  pls  plt  poetry  polynomials  practice  pragmatic  prediction  prepping  preprint  presentation  prioritizing  problem-solving  prof  programming  project  proofs  properties  psychiatry  python  q-n-a  qra  quantifiers-sums  quixotic  quotes  random  rec-math  reflection  research  research-program  retention  retrofit  review  rhetoric  rigor  risk  robust  roots  rust  s:*  s:**  s:***  scholar  scholar-pack  search  serene  skeleton  skunkworks  slides  smoothness  social  soft-question  software  span-cover  spatial  speculation  stamina  state  state-of-art  stories  structure  studying  summary  survey  sv  symmetry  synthesis  system-design  systematic-ad-hoc  systems  tainter  talks  tcs  teaching  tech  technical-writing  technology  techtariat  the-classics  the-great-west-whale  the-monster  the-trenches  the-world-is-just-atoms  thick-thin  things  thinking  threat-modeling  thurston  tidbits  topology  trade  tradeoffs  trees  trends  tricki  tricks  trivia  troll  trust  truth  types  unit  universalism-particularism  unix  vague  vazirani  vcs  video  virtu  visual-understanding  visuo  vitality  von-neumann  web  webapp  wisdom  wordlessness  wormholes  worrydream  worse-is-better/the-right-thing  writing  yoga  zooming  🎓  👳  🔬  🖥  🦉 

Copy this bookmark:



description:


tags: