clarus

As far as I remember, Git was already going strong at the time GitHub appeared. I was also a supporter of Mercurial at first, but I think Git won because:

* it always was fast (written in C vs Python for Mercurial);

* Linus and Linux are behind it.

> Tech is the softest industry ever created.

I am pretty sure that this is the tech people who created this industry and all the jobs evolving around. Softwares are generating a lot of revenue but are incredibly used too.

Pylint and mypy are about syntax and type-checking. While I agree these kind of tools work well, if think that by static analysis people usually imply something which goes farther than that. For example, the languages Facebook is citing (C++, Java, ...) already include type-checking in the compiler.

The fact that Erlang was created for this job does not imply it is the right tool.

For type systems you have Flow and TypeScript, coming with their IDEs. The Chrome devtools and various plugins helps having a good IDE too. Multi threading is possible but rarely used because the concurrency model of JavaScript is event based.

Overall, I think JavaScript has a very rich ecosystem because, if you do Web programming, you do not really have alternatives to JavaScript. So the community made the language support various programming styles, tools and libraries.

I do not believe WASM will help bringing more language to the Web than today because it is already possible to compile to JavaScript with good enough performances for most use cases.

This is very subjective. I feel React is conceptually simpler (no custom templating language) and less opinionated (no official state management system like Vuex for example).

It seems that there are some examples here: https://github.com/CakeML/cakeml/blob/master/explorer/exampl... Whould be cool to have these examples accessible from the web interface of the compiler explorer.

> TypeScript 2.0 goes beyond that and begins to push the envelope on what type systems can do. Recently I've been loving the combination of discriminated union types and nullable types.

As a side node, the FlowType system for JavaScript has had these features for over a year now, while TypeScript 2 is still in beta. These are the exact features which made us decide to go for FlowType instead of TypeScript 6 months ago. Happy to see that these two type systems now converge.

> whereas reasoning about equivalence of JavaScript programs requires carrying out the entire reasoning process in a separate metalanguage

I do not see how you can reason about Haskell in Haskell either, as this is a programming language and not a proof language (maybe I am missing something?).

> Haskell doesn't have a propositional equality type constructor.

This is what I meant. Since with both Haskell and JavaScript you will need to define a propositional equality, in my experience this does not help that much to have a better decidable equality.

I think in any cases you will have to define your notion of equality in the mathematical language you use. Indeed, even in Haskell, the equality operator returns a Haskell boolean but not a proposition, and cannot cope with equality on functions (I guess).

I think the main differences are in the type engines. From what I have seen, Flow can infer much more informations about a program, even on unannotated JavaScript. As a result, with the same amount of annotations, it seems to me that you can find more bugs using Flow than using TypeScript.

With Flow you can also add types gradually. Actually, one of the reasons why Facebook created Flow is that they thought that TypeScript was not "gradual enough". A good presentation on how Flow differs from other type systems: https://www.youtube.com/watch?v=VEaDsKyDxkY

There could be also a third thing:

- continuous evolution of the JS ecosystem towards a cleaner language, with solutions like Flow or TypeScript.

You can get a "kind of Elm" experience on the backend with Flow and JavaScript / NodeJs. The type system of Flow is not as strict as Elm, but you have the main parts (including disjoint unions) and can use existing JavaScript code. With React and Redux you also get a similar framework for the frontend.

It seems that this is also the way of doing things in Elm (from which Redux is inspired): http://guide.elm-lang.org/architecture/index.html . The Update part groups both the definition of the actions and the reducers.

In the community of the theorem prover Coq, a proof obtained by running a proven correct decision procedure is called a "proof by reflection".

There is also the "proof by certificate" approach. You generate a potentially large proof certificate by an unverified program. Then you run a proven correct (small) checker on the certificate to concude that the theorem is correct.

Coq has that too! :) https://coq-bench.github.io/clean/Linux-x86_64-4.02.3-1.2.2/...

I think there are two orthogonal questions:

* Does Apple pretend the FBI cannot access to its devices?

* Can the FBI access to its devices?

The only thing we learn here is the answer to the first question. We know nothing more for the second one.

+1

Are there advantages in developing a new package manager today? There are many mature packaging systems (npm, Bower, Nix, OPAM, ...) which are not written in Go but could probably be adapted to support the Go ecosystem. Moreover, using an existing solution prevents the human cost of debating on "design choices".

candl does not talk about neighbouring countries but about the Golf countries, so he is right.

I do not want to offence anyone, but something which is not said by the article is that the first known inhabitant of this territory were the French. This place was taken by the British at a time of French weakness, exploiting the chaos of the Napoleon's defeat. All that to eventually force the inhabitants out for building a foreign military base, just because (apparently) the British government did not have the will to develop their own nuclear weapons.

As a French, I hope some day we will have a brave enough government who:

* tells the British to refuse to have foreign troops occupying a full territory displacing their own people;

* says that the current situation is wrong, and that these territories are supposed to be French, with the same legitimacy as the Réunion. There is no need to go to war or alike for that, but I feel this is something which should be said.

Talking about the finite group classification, there was a project which achieved to formally prove it correct in Coq for the odd case: http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/

However, having a Coq proof does not mean someone human understand the proof, and the software can evolve in incompatible versions unable to recheck the proof.

By the way, there is also the OPAM package manager for Coq to install Coq and user libraries easily: http://coq-blog.clarus.me/use-opam-for-coq.html

We run into the same kind of challenges to test programs with IO in Coq.io.

To stay pure, we keep the IOs uninterpreted until the compilation (to an OCaml program). We define the tests on the program with uninterpreted IOs. For clarity of the tests, we use an interactive debugger (reusing the tactical mode of Coq) to step through the IO operations. The main advantage of using Coq is that the tests can be made symbolic, thus covering a larger number of cases (if not all the cases). A simple example is explained here: http://coq.io/getting_started.html#use-cases (coincidentally, this is the same example as in this blog post).

What must be trusted in Coq in the kernel, which contains 30,000 lines of code for the latest development version.

It cannot be completely verified by Coq itself due to the Gödel theorem (well, now with this bug this is possible). Still, some part of it can be verified, like the byte-code interpreter. There is actually an ongoing project to make a certified JIT compiler for Coq: http://www.maximedenes.fr/download/coqonut.pdf

Coq itself is already a programming language, but pure in the sense there cannot be any side effects (like IOs). For this pure part there are already an interpreter and a compiler to OCaml, Haskell or Scheme.

To extend Coq with IOs you need to define each new external call. This is basically what is done in the files https://github.com/clarus/coq-chick-blog/blob/master/Computa... and https://github.com/clarus/coq-chick-blog/blob/master/Extract...

No, nothing is done about it, the post contents are not even escaped to generate safe HTML.

By "system call", we do not mean "kernel call" but more "call to the system" in a broader sense, that is from the program to its environment (it could be the OS or other libraries). We should probably use another word since this is confusing.

More exactly, we check that the only calls when the user is not logged in are: ReadFile, ListPosts or Log: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#...

Yes, for now we assume that there is exactly one answer for each external call to the system: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#...

In practice, we should use a timeout in the implementation of all the external calls, but we did not and our model to not enforce it.

Actually this is funny, because "bit" means in French the same thing as "Coq" in English. Probably to be fair we should debate about renaming "bit" also :) (or not).