Nezk

3 ms·

1. 1.▲
   Why Bend 2's typechecker benchmarks are misleading (and its practical flaws)(gist.github.com)

   5 points by Nezk 9d ago|0 comments
2. 2.▲
   by Nezk 10d ago

   And benchmarking this language against Isabelle/Agda/Lean/Rocq is strange. The time taken for those systems to perform their checks is mostly spent on elaboration, which includes unification against metavariables, typeclass r
3. 3.▲
   by Nezk 10d ago

   As I understand it, there are no implicit arguments (and, consequently, no unification) here, right? This doesn't seem very serious given the ambitions of a project like this. Of course, one could argue that it isn't necessary if
4. 4.▲
   by Nezk 4mo ago

   Until a couple of months ago, I was using a Late 2013 MacBook Pro Retina with 4 GB of RAM as my main work computer (and I still use it as a secondary machine). It's amusing to read that some people can't imagine getting by with 4