News for hackers. Stuff that matters.
Re:Coq typeclass resolution is Turing-complete by thaliaarchi on Sunday April 16, 2023 @02:26PM (#35592806)
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 type system and proof system. 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.

Re:Coq typeclass resolution is Turing-complete by haweemwho on Sunday April 16, 2023 @03:03PM (#35593230)
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?

Re:Coq typeclass resolution is Turing-complete by thaliaarchi on Sunday April 16, 2023 @03:16PM (#35593333)
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.
Re:Coq typeclass resolution is Turing-complete by IshKebab on Sunday April 16, 2023 @05:33PM (#35594474)
Yeah I've wondered about that. Especially the obsession with singly linked lists.
Re:Coq typeclass resolution is Turing-complete by User23 on Sunday April 16, 2023 @03:41PM (#35593583)
* * *
Re:Coq typeclass resolution is Turing-complete by thaliaarchi on Sunday April 16, 2023 @03:50PM (#35593665)
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.