clarus

8 ms·

31.
by clarus 7y ago
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+
32.
by clarus 8y ago
The fact that Erlang was created for this job does not imply it is the right tool.
33.
by clarus 9y ago
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 bas
34.
by clarus 9y ago
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).
35.
by clarus 10y ago
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 ex
36.
by clarus 10y ago
> 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 JavaSc
37.
by clarus 10y ago
> 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
38.
by clarus 10y ago
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 func
39.
by clarus 10y ago
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 ca
40.
by clarus 10y ago
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: ht
41.
by clarus 10y ago
There could be also a third thing: - continuous evolution of the JS ecosystem towards a cleaner language, with solutions like Flow or TypeScript.
42.
by clarus 10y ago
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
43.
by clarus 10y ago
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.
44.
by clarus 10y ago
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
45.
by clarus 11y ago
Coq has that too! :) https://coq-bench.github.io/clean/Linux-x86_64-4.02.3-1.2.2/...
46.
by clarus 11y ago
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 secon
47.
The new tactic engine of Coq 8.5(coqhott.gforge.inria.fr)
3 points by clarus 11y ago|0 comments
48.
by clarus 11y ago
+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 a
49.
150,000 penguins die because of giant iceberg(theguardian.com)
1 points by clarus 11y ago|0 comments
50.
by clarus 11y ago
candl does not talk about neighbouring countries but about the Golf countries, so he is right.
51.
by clarus 11y ago
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
52.
by clarus 11y ago
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 Co
53.
by clarus 11y ago
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
54.
by clarus 11y ago
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 t
55.
by clarus 12y ago
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, so
56.
Proving false in Coq using an implementation bug(github.com)
125 points by clarus 12y ago|61 comments
57.
by clarus 12y ago
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
58.
by clarus 12y ago
No, nothing is done about it, the post contents are not even escaped to generate safe HTML.
59.
by clarus 12y ago
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 anoth
60.
by clarus 12y ago
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 i

More ›