Cladode

I agree with what you write.

But I also believe the counterfactual that, had Sun/Oracle been based their language upon (core) ML rather than Java (with suitable pragmatic additions like code loading and been able to convince programmers to use it), then that language would be even more dominant and performant today. Many of Java's mistakes and detours would have been avoided from Day 1.

Can I prove this? No. But the fact that Java and essentially all other successful languages have gradually been adapting essentially all of ML (sans modules), is evidence. It means that language designers like G Bierman, A Hejlsberg, Odersky et al, too have gone Milner's way.

   pros/cons 

The main issue is proof automation. Curry-Howard based provers (Coq, Agda, Lean etc) are nice for teaching but if you want to get work done (e.g. you want to verify an OS kernel), you need to automate as much as possible. Isabelle/HOL currently has by far the most powerful automation. This is partly because, like Coq, it is an old system (unlike Lean and Agda) and lots of automation has been built in the past, but also because a lot of automation is much easier to adapt to provers based on classical logic (as opposed to the constructive logics that Curry-Howard needs (yes, I know that classical reasoning can be done within constructive logic)). Adapting proof automation that has been available for a while for Isabelle/HOL to Curry-Howard is at least in parts an open research problem. Lean has been created in parts because of the urgency of given Curry-Howard systems much better proof automation.

There is an additional dimension which is strength of the logic at hand. The logics Coq, Lean et al are based on are more expressive in various dimensions. Whether that's relevant to your use case depends on what kind of maths you are trying to formalise. If it is higher category theory, it matters a great deal, for program verification it tends not to be important b/c most program verification can be done in rather weak logics.

Nobody has credible data enabling reproducible comparison of programming languages. The big lacuna of PL research ...

If popularity mattered ... PHP, JavaScript etc.

I find the evolution of all successful programming languages eventually to evolve into an ML-like core fascinating.

If we collapse the two concepts of

- best possible X

- most popular X

are we loosing possibly interesting perspectives on X?

   Worked out pretty well, I think.

Au contraire mon ami!

ML was better than most of its successors, including Java, which held programming back. Milner's ML avoided some of Java's glaring mistakes (e.g. exception specifications, lack of generics, non-uniform treatment of types, lack of higher-order functions, lack of pattern matching) from the start. Xavier Leroy showed how efficiently to compile ML in the 1990s.

The main thing ML lacked (w.r.t sequential computing), was a good integration with OO and HKTs. That was solved by Scala.

Thanks.

We were talking cross-purposes. I was thinking about partially initialized arrays in the context of a Rust-like type-checker. I don't think the analysis you ran in 1981 in a prover is possible in 2020 in a type-checker, at least without putting most of the bits dealing with partial initialization into unsafe-boxes.

It would be great if Rust-style type-based lifetime analysis could cope with partial initialization.

   partially initialized arrays

I agree that partially initialized data structures are important for low-level, performance-oriented programming. But it is not clear how to do this within a Rust-style type-based approach to memory safety. Naturally, one can always wrap the problematic code that deals with partially initialised data in an unsafe-block, but you can already do that in Rust. By Rice's theorem we know that we cannot have a feasible typing system that allows us always to deal with partially initialised data in a safe way, but could there be a compromise, covering most of the standard uses of partially initialised data (e.g. what you find in a standard algorithm text book like CLRS, or a standard library like C++'s)? I don't see how right now, because the order of initialisation can be quite complex, too complex to fit neatly into well-bracked lifetimes a la Rust.

Have you got any ideas how to do better?

Albert Cohen from Google gave a really good lecture on polyhedral compilation in the real world at PLISS [1] this year: slides [2], lecture videos [3, 4].

A core problem of the polyhedral approach, is that the thing that makes it so appealing (it being expressive enough to enable the many interesting program transformations), is costly for large programs making, the overall optimisation process and hence the compiler hard to scale. Naturally, this difficulty makes for interesting research problems.

[1] https://pliss.org/

[2] https://pliss2019.github.io/albert_cohen_slides.pdf

[3] https://www.youtube.com/watch?v=mt6pIpt5Wk0

[4] https://www.youtube.com/watch?v=3TNT5rFVTUY

   Did you try tags? 

No. I found that many of my early ideas on how to structure my notes didn't scale, made evolution of my system more difficult. So later I tried not to impose addition structure. Tagging enforces a structure, and how I classify ideas changes over time. What do tags give that grepping words doesn't?

That's a good question. I tried a variety of options, but it stabilised on something that could be termed "micro-summary of context as file name". Example:

   - giraffes.html
   - giraffes_in_history.html
   - natural_predators_of_giraffes.html
   - grade_inflation.html
   - graffiti.html
   - genghis_khan.html       
   - grassroots_lobbying.html

Since all my Zettel are version controlled anyway, I don't see the point of tracking dates/times in filenames (or the file itself). I've now got so many Zettel that I can no longer recall even descriptive names like the above anyway: is the Zettel called giraffes_in_history.html or history_of_giraffes.html ...? So in practise, nowadays, when I look for related Zettel I always use grep with words I expect to be in the relevant Zettel. Example:

   grep -i giraffe *.html

It works really well.

What I do recommend is writing a little tool that produces filenames in a consistent way. (E.g. stripping out 'weird' characters, removing capitalisation etc.) I found that the more uniform filenames, file structure etc, the easier searching remains. Moreover, writing tools that mine / transform Zettel is also easier when the setup is uniform.

I also tried adding structures by subdirectories

   - computer_science
   - economics
   - biology

etc, but that didn't scale, since everything is connected to everything else. Knowledge is not tree- or DAG-structured. Flat file structure + hyperlinks works for me.

I've been using a system like that successfully as an academic (for some interpretation of successful). Started when I was a PhD student 25 years ago, and have been maintaining it ever since. I was inspired by Niklas Luhmann's Zettelkasten, whom I read voraciously as a teenager. I started as an undergraduate with hand-written index cards, but the obvious advantages of electronic files (fast search, cut/paste, easy backup, doesn't need physical space) were immediately clear to me, so I moved to a computer-based system. As I had already been burned by proprietary formats before, I use html as format from day one, every index card is html file in a separate directory. This has various advantages, including

- Easy consistent styling through css

- No WYSIWYG, separation of content and styling

- Easy to include code, which sits in the directory associated with the index card

- Easy to cross link

- Easy to backup

- Everything is under git control

- Easy to write shell scripts / programs that automate various tasks related to my notes

- Search with standard tools like grep

- Edit in my favourite text editor (Org-mode for quick drafting is especially useful I find)

- High quality rendering through modern browsers

- Easy to cut and paste into emails, whatsapp skype discord etc which is how I communicate with students and colleagues

- Easy to include other formats like images sound video etc

- Since the emergence of MathJax I can use LaTeX markup which means I can cut-and-paste between my index cards, scientific papers and lecture notes/slides

In summary, I'm super glad I didn't go super-hi-tech and stuck with marked-up text. It was the right choice! As Graydon Hoare once wrote: "[A]lways bet on text." How much work is it? I spend 1-2 hours on average every day on writing. Is it worth my time? What are the advantages for me that keep me using such a system?

- Structured, easily accessible 'idea store' / second-memory for later refinement and reuse. Refinement is maybe even the core: when I come back to a subject years later I come back from a different angle

- Helps writing introductory sections in papers, because I will have sketched my understanding of a subject already on an index card

- Helps writing related work sections in papers, because I accumulate work related to any particular index card's subjects over years

- Makes reviewing papers much easier, because I can cut-and-paste missing related work (most scientific papers are written by PhD students and post-docs who lack a historical perspective)

- Communicating with students: as an academic I get new students every year, and since they got through similar stages and problems, it has become easy to reuse what I wrote in paste years

- The most important: cultivating a habit of writing down ideas, writing about ideas in a structured way, breaking them down into smaller parts etc, all of which helps me to understand things better, and to communicate them more clearly to others

Is it worth it? I ask myself this question every day. I found that in the first few years, I could always remember what I had written, so my system was of limited use. That changed after about 8 years, when I could no longer recall most of what I had written down, and then it became rather useful, since I got 'new' and already pre-digested ideas.

For me the biggest problem is that it has also become a procrastination device: I love writing. Whenever I am stuck with a work problem (and that happens a lot), I have a tendency to procrastinate by writing long entries on obscure subjects, unrelated to my work. It feels like work, in some sense it is work, but it lets me avoid confronting high-priority tasks head on.