Jaxan

27 ms·

361.
by Jaxan 7y ago
To me it means that there is a formal semantics (for example in Coq), and that we can formally prove properties of the code. There does not seem to be a semantics here.
362.
by Jaxan 7y ago
I like how they incorporate an SMT solver. They claim: “all code is proven”. What does that mean? What is proven about the code? Absence of memory bugs, or actual correctness of algorithms?
363.
by Jaxan 7y ago
Sometimes it’s easier to remember the why than the what. Then it does make sense to learn about it!
364.
by Jaxan 7y ago
Microsoft does this. They are reimplementing a lot of internet protocols using Fstar. So not only bounds checking, but also verified. But it’s a huge undertaking!
365.
by Jaxan 7y ago
The website is a bit glitchy on my phone. Whenever I scroll, it zooms out a bit, which is disorienting.
366.
by Jaxan 7y ago
The moment you take a picture, your camera or phone already does tons of editing. Like really a lot! I assume, you wouldn’t consider that “photoshopping”. Where do you draw the line? For me, haze removal, water removal are like white balanc
367.
by Jaxan 7y ago
A good alternative is KaTeX. That one doesn’t require JavaScript.
368.
by Jaxan 7y ago
I’m not even sure what to think of the term “algorithmic sorting.” Is quicksort considered as algorithmic sorting ... ?
369.
by Jaxan 7y ago
Then what is adorable about it? I was imagining cute animals would appear in the terminal. This is not the case?
370.
by Jaxan 7y ago
As said in the abstract: another gradient optimizer!
371.
by Jaxan 7y ago
There was Objective-C++, which combined Objective-C and C++. You could literally write both languages mixed together. Honestly, it was a Frankenstein monster. The semantics were very vague (especially since C++ uses raii and obj-c uses refe
372.
by Jaxan 7y ago
Interesting idea. It makes you wonder how to best spend your time: writing better software (ie less bugs), or invest time in fuzzification (ie less exploits).
373.
by Jaxan 7y ago
Maybe this is well known, but it's still worth repeating (like many things which are true are worth repeating). As a young researcher, I like Vardi's short essays a lot. He has some historical perspective which many of my peers do
374.
by Jaxan 7y ago
Well building the reals from rationals is not easy at all. It took a few decades to get a reasonable definiton. And in constructive mathematics, there are several competing (non equivalent) definitions of the reals. It's a very deep to
375.
by Jaxan 7y ago
Yeah, you would think so (and I thought the same for a while). All the epsilon delta stuff seems to work fine with rationals. But really most theorems of calculus (intermediate value thm, etc...) just are false, with very easy counter examp
376.
by Jaxan 7y ago
One possible answer is that any algorithm can be sped up linearly: https://en.m.wikipedia.org/wiki/Linear_speedup_theorem . (At least theoretically, for runtimes bigger than linear.) Another answer could be Moore'
377.
by Jaxan 7y ago
Last time it happened (7 years ago), two people died.
378.
by Jaxan 7y ago
Thanks for linking to the repo. I just had a look. It's impressive how many github users want to be funny and make bullshit pull requests and nonsense issues. What is the point of doing all that :-(?
379.
by Jaxan 7y ago
I don't really know Racket. But from what i've seen, it's mostly sold as a language to create new languages in. Rascal on the other was designed to analyse existing languages. They wanted to have a single framework to analyse
380.
by Jaxan 7y ago
TeX live is a distribution and it comes with many things (TeX, LaTeX, ConTeXt, fonts, ...). Both LaTeX and ConTeXt are built on top of bare TeX and add lots of features. I have used ConTeXt a quite a bit, and it seems to be more designed to
381.
by Jaxan 7y ago
This was actually done with ConTeXt, not LaTeX.
382.
by Jaxan 7y ago
Because you spend more time on it? My reading is definitely slower than youtube videos. And still a bit slower than most lectures.
383.
by Jaxan 8y ago
Coq is a good example of a non-Turing complete programming language.
384.
by Jaxan 8y ago
Yes the theorem holds for any base.
385.
by Jaxan 8y ago
To me the advantage is that it works in any browser. So I don’t have to set up anything. It evens works on mobile.
386.
by Jaxan 8y ago
But in what order should they come!?
387.
by Jaxan 8y ago
I don’t think GitHubs list is good either. It only contains open source software (right?) and does not account for any in-house software by big enterprise companies (and I think that those are still the biggest).
388.
by Jaxan 8y ago
17 is a bottom element?
389.
by Jaxan 8y ago
I would say an exception is much more convenient. Buggy code that silently continues to run is very hard to debug!
390.
by Jaxan 8y ago
Since English is only third most spoken language, why would they adopt English?

More ›