As a programming language enthusiast, continuously following the news in this topic : i thought i would know about any ongoing serious project of good programming language development. And sneaky JetBrains proved me wrong. All from nowhere they suddenly announce Arend 1. Arend seems to me to be a very professionally designed programming language. With very modern type system ["homotopy"]. To give you some reference : not even F* or Idris 2 are going to support homotopy type theory, at least according to my poor knowledge. The closest competitor of Arend is Microsoft's Lean and Agda. Being JetBrains we expect good IDE support for it. And we would be right, as the IDE already now, at the start is perhaps the best among well designed programming languages. Too fantastic to be true? Yes. It has a tiny deficiency : it is not designed to create executables, one can not execute Arend programs. It is only for modelling and verification. Yet. But i am still very happy about this development, as i am very optimistic that executability will come to Arend over time and i interpret this development as one more stepping stone towards modern programming. With this JetBrains is only the second firm to have created a professionally designed programming language with powerful type system, Microsoft being the first perhaps with F* and Lean.
Friday, August 9, 2019
Thursday, June 13, 2019
Monday, May 20, 2019
Guix 1 released
Guix 1 released.
Guix is the other functional package manager and operating system distribution, beside the more popular Nix.
Guix is the other functional package manager and operating system distribution, beside the more popular Nix.
Thursday, March 7, 2019
maybe a solution of boolean blindness
the Maybe type can sometimes solve the boolean blindness problem better then a renamed Bool datatype
Tuesday, March 5, 2019
Selective Applicative Functors
A new abstraction between applicative and monadic functors.
[You need a confident understanding of the applicative and monad interfaces to understand this article.]
https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf
[You need a confident understanding of the applicative and monad interfaces to understand this article.]
https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf
Saturday, February 16, 2019
ai for bug detection
is just a hype
artificial intelligence is big hype now, it deserves it, it deserves even more hype than it gets; but particularly for software bug detection it is a wrong idea; for that it is just an instance of the (i have a cool hammer so everything is a nail) fallacy
the tool for bug detection is the type system; type systems and type theory in math and programming were invented exactly to catch human mistakes; in this article i will compare ai and type system
currently type systems are much underused; the haskell programming language is the one that has the best type system [among production-strong languages], by far, but even its type system is much outdated [just think about the fact that it does not even have dependent types]; the potential update of our type systems used in practice is very easy, much overdue and would decrease the number of bugs by several orders
ai is black box; even after substantial experience with one particular ai algorithm : the programmer remains unsure which bugs it catches; with type system the programmer knows exactly, surely, what properties of the program are ensured, he can use this info to strengthen the properties of the program which are not covered by the type system by unit testing or more attention, more documentation
type theory is a foundational field of mathematics and is more than a century old; artificial intelligence [especially the widely successful part] is about 1-2 decades old; and the theory of ai for bug detection is almost non-existent; i see, one can point out many scientific articles in the topic, but that does not make it a scientific field, let alone a successful one
type checking is an order of magnitude faster than an ai algorithm
the type system pinpoints the error at the right location
the type system helps in a lot of other tasks too : editing the code, documenting the code, automatic implementation
from a more general point of view the best direction for the software development world to decrease the bugs is correctness by construction
artificial intelligence is big hype now, it deserves it, it deserves even more hype than it gets; but particularly for software bug detection it is a wrong idea; for that it is just an instance of the (i have a cool hammer so everything is a nail) fallacy
the tool for bug detection is the type system; type systems and type theory in math and programming were invented exactly to catch human mistakes; in this article i will compare ai and type system
currently type systems are much underused; the haskell programming language is the one that has the best type system [among production-strong languages], by far, but even its type system is much outdated [just think about the fact that it does not even have dependent types]; the potential update of our type systems used in practice is very easy, much overdue and would decrease the number of bugs by several orders
ai is black box; even after substantial experience with one particular ai algorithm : the programmer remains unsure which bugs it catches; with type system the programmer knows exactly, surely, what properties of the program are ensured, he can use this info to strengthen the properties of the program which are not covered by the type system by unit testing or more attention, more documentation
type theory is a foundational field of mathematics and is more than a century old; artificial intelligence [especially the widely successful part] is about 1-2 decades old; and the theory of ai for bug detection is almost non-existent; i see, one can point out many scientific articles in the topic, but that does not make it a scientific field, let alone a successful one
type checking is an order of magnitude faster than an ai algorithm
the type system pinpoints the error at the right location
the type system helps in a lot of other tasks too : editing the code, documenting the code, automatic implementation
from a more general point of view the best direction for the software development world to decrease the bugs is correctness by construction
Subscribe to:
Comments (Atom)