Cladode

7 ms·

31.
by Cladode 7y ago
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 programmer
32.
by Cladode 7y ago
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 pos
33.
by Cladode 7y ago
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
34.
by Cladode 7y ago
If we collapse the two concepts of - best possible X - most popular X are we loosing possibly interesting perspectives on X?
35.
by Cladode 7y ago
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 specifica
36.
by Cladode 7y ago
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 leas
37.
by Cladode 7y ago
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 saf
38.
by Cladode 7y ago
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 appeali
39.
by Cladode 7y ago
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,
40.
by Cladode 7y ago
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_preda
41.
by Cladode 7y ago
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 Ze