Hacker News Reader

Comment by thaliaarchi | Hacker News Reader

Author here! I had a hunch that the typeclass resolution engine in the Coq typechecker could be Turing-complete, so I proved it by implementing a variant of Brainfuck in it. Feedback welcome.

View on HN

Not a feedback, question. How do you feel doing work like this in a world where people see javascript as a acceptable language? Second, somewhat related, what would be the biggest problem preventing wide, industry adoption of Coq/other formal methods?

I think there are varying levels of assurance that developers need while writing software. I tend towards stricter languages with more guarantees, like Rust with its borrow checker and Coq with its powerful types and proofs. This doesn't need to be a universal preference, though; my preferred work is in compilers, which requires a high degree of assurance, and I study programming languages formally.

The largest barrier to greater adoption of languages like Coq with proof systems built-in is the formal background needed to get started. I think that Rust has done an excellent job at making stronger systems more accessible, but it takes a lot of conscious work.

With JavaScript, I think the idea that performance in language design can be an afterthought, made up for by world-class optimizing JIT compilers, is fundamentally wrong. It doesn't give users a meaningful way to easily reason about the performance of the programs they write. The main implementation of Python, pythonc, is essentially an interpreter over an unoptimized bytecode format, giving it poor performance. I think performance considerations should be a fundamental part of the language design.

Thanks for your perspective.

I'm wondering how this squares with the tendency of formal language theory folks to push for functional languages. It's clearly a preferred approach if rigorous correctness is your main goal, but don't functional languages like Haskell suffer from the fundamental issue that reasoning about runtime performance is really hard?

Haskell is notoriously difficult to reason about runtime performance, but that is due to its lazy evaluation, not because it is functional. Lazy evaluation can cause hidden space leaks, where expressions have not yet been evaluated, so maintain references to other values. Most functional programming languages are not lazy.

Yeah I've wondered about that. Especially the obsession with singly linked lists.

> The largest barrier to greater adoption of languages like Coq with proof systems built-in is the formal background needed to get started.

I believe this to be a language problem and not a conceptual problem. All that you need to pragmatically formalize semantics is Hoare triples and basic predicate calculus[1]. Anyone that can understand an if statement already has the necessary conceptual machinery. The so-called “formal methods” community delights in over complicating the problem with gadgets like category theory. Which is ironic, because they’re introducing the same kind of unnecessary complexity that causes the problem that they’re trying to solve.

[1] ok that’s not utterly strictly true because arrays (or mutable functions, as I like to think of them) present some subtleties, but those are more a problem for the definers rather than the users.

I was referring to how the communities of these languages typically frame the problem, so you need formal background to read the materials published on it. As you say, this is a major barrier. This is where Rust shines, in that they've framed the language in terms of how its used, developed accessible documentation, and steered away from delving into the theory behind it.

I don't think people find Javascript an acceptable language. The meteoric rise of TypeScript proves that.

I have met and seen online a lot of people that see no problems with vanilla Javascript. I honestly don't even know where to begin here.

I’m shocked you didn’t just start with white space. ;)

I’m excited to dig through this more. Nice work!

Reply on news.ycombinator.com