[HN Gopher] Why don't you use dependent types?
___________________________________________________________________
Why don't you use dependent types?
Author : baruchel
Score : 160 points
Date : 2025-11-02 15:06 UTC (7 hours ago)
(HTM) web link (lawrencecpaulson.github.io)
(TXT) w3m dump (lawrencecpaulson.github.io)
| fluffypony wrote:
| Agree with this. The punchline here is not "dependent types bad",
| it is "choose your battles". Isabelle/HOL pushed frighteningly
| far without proof objects or dependent types, from schemes to
| BSG, and never hit the mythical wall. What moved the needle was
| automation, libraries, and legible proofs, not a fancier core
| calculus. Lean is great, but if the toolchain bogs down and
| equality games leak into your day, your fancy types are like
| Tesla FSD: impressive demo energy, unpredictable commute (no
| offense to anyone who uses it regularly). Knowing when not to use
| them is the real superpower imho.
|
| If you need finely indexed invariants, sure, reach for DT. For
| the other 95%, HOL plus type classes and locales, backed by a
| small kernel and big libraries, will get you to production faster
| and with fewer regrets. Milner's LCF insight still pays the
| bills. And yes, croissants are delicious, but optional axioms are
| a risky breakfast.
| lacker wrote:
| Dependent types are very useful for some things. For example, I
| wish Python had the ability to express "a 10 x 5 matrix of
| float32s" as a type, and typecheck that.
|
| The Curry-Howard correspondence, using dependent type system to
| have "proofs" be equivalent to "types", is powerful, but it can
| be really confusing. From a human point of view, there is a huge
| difference between "Your proof is wrong" and "You wrote a
| statement that fails typechecking".
|
| Intuitively, when you make an error with types, it should be
| something fairly trivial that you just read the error and fix it
| up. When you make an error in a proof, it's understandable if
| it's very complicated and requires thought to fix. The natural UI
| is different.
|
| So I agree with the author that the greatest benefit of Lean is
| not its typesystem per se, but its community. Specifically the
| fact that Lean's library of mathematics, mathlib, is organized
| like an open source community with pull requests. Whereas
| Isabelle's library of mathematics, the AFP, is organized like a
| scientific journal with referees.
|
| I'm working on a dependent type system at the moment for a new
| theorem prover - Acorn, at https://acornprover.org - and my hope
| is to combine the good points of both Lean and Isabelle. It's
| nice that Lean has the power to cleanly express the simple
| dependent types that mathematicians often use, like vector spaces
| or quotients. But if you use dependent types too much then it
| does get complicated to debug what's happening.
| Sharlin wrote:
| > For example, I wish Python had the ability to express "a 10 x
| 5 matrix of float32s" as a type
|
| To clarify, as long as 5 and 10 are constants, this is entirely
| possible in C++ and Rust^1, neither of which are dependently
| typed (or at most are dependently typed in a very weak sense).
| In general, neither can ensure at compile time that an index
| only known at runtime is in bounds, even if the bounds
| themselves are statically known. A proper dependently-typed
| language can prevent runtime out-of-bound errors even if
| _neither_ the indices nor the bounds are known at type check
| time.
|
| ^1 And weakly in many other languages whose builtin array types
| have compile-time bounds. But C++ and Rust let _user-defined_
| generic types abstract over constant values.
| etbebl wrote:
| The latter is what would be most useful imo. Even Matlab can
| type check matrix sizes with constants these days, but I
| often wish I could use variables to express relationships
| between the sizes of different dimensions of inputs to a
| function.
| zozbot234 wrote:
| Yes, the point of dependent types is that they give you the
| ability to do some sort of almost arbitrary (though not
| strictly Turing-complete) "computation" as part of type
| checking, which essentially dispenses with the phase
| separation between "compiling" and "running" code - or at
| least makes compile-time computation unusually powerful. So
| if you want to replicate the properties of dependent typing
| in these existing languages you'll need to leverage their
| existing facilities for compile-time metaprogramming.
|
| > A proper dependently-typed language can prevent runtime
| out-of-bound errors even if neither the indices nor the
| bounds are known at type check time.
|
| Yes, but the way this is done is by threading a proof "this
| index is within bounds" throughout the code. At runtime (e.g.
| within 'extracted' code, if you're using common dependently-
| typed systems), this simply amounts to relying on a kind of
| capability or ghost 'token' that attests to the validity of
| that code. You "manufacture" the capability as part of an
| explicit runtime check when needed (e.g. if the "index" or
| "bounds" come from user input) and simply rely on it as part
| of the code.
| gpderetta wrote:
| You can do arbitrary computations as part of type checking
| in C++, yet I don't think it should be considered
| dependently typed.
|
| It seems to me that dependent typing strictly requires
| going from runtime values to types.
|
| (You can parametrize types by runtime values in c++ in a
| trivial sense, by enumerating a finite set a compile time
| and then picking the correct type at runtime according to a
| runtime value, still I don't think it counts as the set of
| valid types would be finite).
| zozbot234 wrote:
| The "runtime" values of a dependent type system are not
| quite runtime values either, because the computation is
| happening at compile time. When you "extract" a program
| from a dependently-typed to an ordinary programming
| language that can compile down to a binary, the dependent
| types are simply erased and replaced with ordinary, non-
| dependent types; though there may be "magic" casts in the
| resulting program that can only be proven correct via
| dependent types.
| lacker wrote:
| That's a good point, for example in Eigen you can do
|
| Eigen::Matrix<float, 10, 5>
|
| I just really want it in _Python_ because that 's where I do
| most of my matrix manipulation nowadays. I guess you also
| would really like it to handle non-constants. It would be
| nice if these complicated library functions like
|
| torch.nn.MultiheadAttention(embed_dim, num_heads,
| dropout=0.0, bias=True, add_bias_kv=False,
| add_zero_attn=False, kdim=None, vdim=None, batch_first=False,
| device=None, dtype=None)
|
| would actually typecheck that kdim and vdim are correct, and
| ensure that I correctly pass a K x V matrix and not a V x K
| one.
| zozbot234 wrote:
| Python is a dynamic language where everything happens at
| run time, including checks of variable types. So you can
| already do this.
| nephanth wrote:
| Python has static typechecking which, while not perfect,
| works pretty well as long as you're not actually trying
| to circumvent it (or manipulating things "too
| dynamically")
| bluGill wrote:
| The problem with runtime is when you make a mistake it
| can be a long time before you find out. Compile time
| means a large class of problems is prevented without
| perfect test coverage. On a small project it isn't a big
| deal but when you have hundgeds of developers over
| decades you will miss something
| thomasahle wrote:
| You can do that in python using https://github.com/patrick-
| kidger/torchtyping
|
| looks like this: def batch_outer_product(x:
| TensorType["batch", "x_channels"],
| y: TensorType["batch", "y_channels"]
| ) -> TensorType["batch", "x_channels", "y_channels"]:
| return x.unsqueeze(-1) * y.unsqueeze(-2)
|
| There's also https://github.com/thomasahle/tensorgrad which
| uses sympy for "axis" dimension variables:
| b, x, y = sp.symbols("b x y") X = tg.Variable("X", b,
| x) Y = tg.Variable("Y", b, y) W =
| tg.Variable("W", x, y) XWmY = X @ W - Y
| patrickkidger wrote:
| Quick heads-up that these days I recommend
| https://github.com/patrick-kidger/jaxtyping over the older
| repository you've linked there.
|
| I learnt a lot the first time around, so the newer one is
| much better :)
| thomasahle wrote:
| Ah, I would have never thought jaxtyping supports torch
| :)
| uecker wrote:
| C has such types and can guarantee that there is no out-of-
| bounds access at run-time in the scenarios you describe:
| https://godbolt.org/z/f7Tz7EvfE This is one reason why I
| think that C - despite all the naysayers - is actually
| perfectly positioned to address bounds-safe programming.
|
| Often in dependently-types languages one also tries to prove
| at compile-time that the dynamic index is inside the dynamic
| bound at run-time, but this depends.
| turndown wrote:
| I thought that this was a GCC extension(you need to use
| #define n 10 instead of int n = 10). Is this not the case
| anymore?
| uecker wrote:
| This is in ISO C99. In C11 it was made an optional
| feature but in C23 we made the type part mandatory again.
| Sharlin wrote:
| -fsanitize-bounds uses a _runtime_ address sanitizer,
| surely? The program _compiles_ fine. In a (strongly)
| dependently typed language, something like the following
| would refuse to typecheck: int foo(int i) {
| int bar[4] = { 1, 2, 3, 4 }; return bar[i]
| }
|
| The type checker would demand a proof that i is in bounds,
| for example int foo(int i) { int
| bar[4] = { 1, 2, 3, 4 }; if i < 4
| return bar[i] else return 0
| }
|
| In languages with an Option type this could of course be
| written without dependent types in a way that's still
| correct by construction, for example Rust:
| fn foo(i: 32) -> i32 { let bar = [1, 2, 3, 4];
| bar.get(i) // returns Option<i32>, not a raw i32
| .unwrap_or(0) // provide a default, now we always have an
| i32 }
|
| But ultimately, memory safety here is only guaranteed by
| the library, not by the type system.
| uecker wrote:
| You seem to be repeating what I said except you mixup
| strong and static typing. In a statically dependent-typed
| language you might expect it this not to compile, but
| this also depends. Run-time checking is certainly
| something you can combine with strong dependent typing.
|
| Implementing bounds checking that returns option types
| (which can also implement in C) is not exactly the same
| thing. But dependent typing can be more elegant - as it
| is here.
| uecker wrote:
| Update: For the interested, here are three ways to write
| this in C, the first using dependent type, the second
| using a span type, and the third using an option type.
| All three versions prevent out-of-bounds accesses:
| https://godbolt.org/z/nKTfhenoY
| saghm wrote:
| > In general, neither can ensure at compile time that an
| index only known at runtime is in bounds, even if the bounds
| themselves are statically known.
|
| Yeah, this seems like matrixes might not be a great first
| example for explaining the value of dependent types. It's
| fully possible to define a matrix that uses a generic type as
| the index for each dimension that doesn't allow expressing
| values outside the expected range; it would just be fairly
| cumbersome, and the usual issues would creep back in if you
| needed to go from "normal" integers back to indexes (although
| not if you only needed to convert the indexes to normal
| integers).
|
| I find that the potential utility of dependent types is more
| clear when thinking about types where the "dimensions" are
| mutable, which isn't usually how I'd expect most people to
| use matrixes. Even a simple example like "the current length
| of a list can be part of the type, so you define a method to
| get the first element only on non-empty lists rather than
| needing them to return an optional value". While you could
| sort of implement this in a similar as described above with a
| custom integer-like type, the limitations of this kind of
| approach for a theoretically unbounded length are a lot more
| apparent than a matrix with constant-sized dimensions.
| jyounker wrote:
| The advantage of dependent typing systems is that you can
| say that the arguments to a matrix multiplication function
| must have dimensions (m, i) and (i, n) and that result will
| have dimensions (m, n).
| tmtvl wrote:
| In Common Lisp: (defparameter *test-array*
| (make-array '(10 5) :element-type 'Float
| :initial-element 0.0)) (typep *test-array* '(Array
| Float (10 5)))
|
| And the type check will return true.
| ndr wrote:
| Compile-time checks is what's implied in virtually all
| these conversations.
|
| Does that check run at compile time?
| tmtvl wrote:
| If I define a function foo which takes an (Array Float
| (10 5)) and then define a function bar which uses the
| result of calling foo with an (Array String (3 3)) then
| SBCL will print a warning. If I don't redefine foo and
| call bar with such an array then a condition will be
| raised. It's not quite the same as, say Rust's 'thing
| just won't compile', but that's due to the interactive
| nature of Common Lisp (I believe someone called it the
| difference between a living language and a dead language
| (though the conventional meaning of living language and
| dead language in programming is a bit different)).
| thesz wrote:
| "In general, neither can ensure at compile time that an index
| only known at runtime is in bounds, even if the bounds
| themselves are statically known."
|
| I remember being able to use telescopes [1] in Haskell long
| time ago, around 2012 or so.
|
| [1] https://www.pls-lab.org/en/telescope
|
| Haskell was not and is not properly dependently typed.
| aatd86 wrote:
| > using dependent type system to have "proofs" be equivalent to
| "types"
|
| Do you mean proposition as types? And proof has a program?
|
| Or do you see it at somewhat a higher order, since values are
| proof for a type, and types can perhaps be proof at a higher
| level if they are first class citizen in the language?
|
| (Which makes me think that dependent types is really a stairway
| between two type systems?)
|
| Just wondering, since I had never personally seen it described
| in that fashion.
|
| Other question: What is the function and runtime treatment of
| dependent types? Can they be instantiated on the spot by
| runtime values? A bit like defining/declaring functions that
| return arrays of runtime-known length? Does it involve two
| aspects of type checking? compile and runtime? Implementation-
| wise, doesn't it require too many indirections?
| akst wrote:
| One of the things I love about typescript is if your audacious
| enough you can kind of make some types like this (still a far
| cry from dependent types):
|
| https://github.com/AKST/analysis-notebook/blob/main/lib/base...
| (Line 38)
|
| It type checks, but I haven't gotten a lot of mileage out of
| this (so far at least). I did something similar for vectors,
| which has been useful for when I destructure the elements, and
| it preserves that through vector operations.
|
| https://github.com/AKST/analysis-notebook/blob/777acf427c65c...
|
| The same is actually applies true for matrices, I wrote the
| multiplication to carry the new size into the output type
|
| https://github.com/AKST/analysis-notebook/blob/777acf427c65c...
|
| That said I mostly use this for square matrixes in web GL so
| you're mostly working with square matrixes.
|
| As an aside, this source is from a toy project largely more for
| leisure and fun, I don't know if something like this would be
| suitable for a larger more data oriented project (at least in
| trend of how I represent data here).
| olivia-banks wrote:
| I did a small small experiment in dependent typing for Python
| (and catching those errors before run time). It's a decently
| good fit, and with HM Type inference some neat things just fall
| out of the design.
|
| But the real challenge is deciding how much of Python's
| semantics to preserve. Once you start enforcing constraints
| that depend on values, a lot of idiomatic dynamic behavior
| stops making sense. Curious what ways there are to work around
| this, but I think that's for a person better at Python than I
| :)
| pron wrote:
| It's interesting just how much of the debate in modern logic
| boils down to aesthetic preferences. On the other hand, I guess
| that if there were overwhelming practical advantages, there
| wouldn't be much to debate...
|
| BTW, here's a "discussion paper" by Paulson and Leslie Lamport
| about typing in specification laguages from 1999:
| https://www.cl.cam.ac.uk/~lp15/papers/Reports/lamport-paulso....
| Paulson represents the "pro-type" view, but note that since that
| paper was written, there have been developments in mechanised
| theorem proving of untyped formalisms, including in Lamport's own
| (TLA+).
| paulddraper wrote:
| I wouldn't call it "aesthetics" per se.
|
| More like "No free lunch."
|
| You can gain advantages, e.g. more complete compile time
| guarantees, but at disadvantages, e.g. greater program
| complexity, or longer compile times.
|
| The subjectivity is whether the tradeoff is "worth" it.
| griffzhowl wrote:
| Great, I love this stuff.
|
| See here for a summary of the many results of the author and
| team's research project on formalization:
|
| https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/
|
| Especially interesting for me is the work on formalizing quantum
| computing algorithms and theorems (open access):
|
| https://link.springer.com/article/10.1007/s10817-020-09584-7
| anonzzzies wrote:
| You just prove / use dependently typed languages / tla+ where it
| makes sense, not for _everything_. The latter might make sense if
| it 's mostly automated maybe, but it takes really painful
| elaborate work to get full coverage and for sure most stuff
| really doesn't need that. I always think these formal methods +
| unit/integration tests cover so much that you are already far
| more robust than most on earth.
| cwzwarich wrote:
| The bigger problem with HOL (or simple type theory) is not the
| lack of dependencies, but rather the lack of logical strength.
| Simple type theory is equivalent in logical strength to bounded
| Zermelo set theory (i.e. ZF without Foundation or Replacement,
| and with Separation restricted to formulas with bounded
| quantifiers). This is unfortunately too weak to formalize post-
| WW2 mathematics in the same style as is done by ordinary
| mathematicians. Similarly, it does not offer a great way to deal
| with the size issues that arise in e.g. category theory.
| zozbot234 wrote:
| You can always add axioms to improve logical strength. For
| example, one common approach for dealing with size issues in
| set theory is positing so-called 'inaccessible cardinals' which
| amount to something quite similar to the 'universes' of type
| theory.
| cwzwarich wrote:
| Adding axioms to simple type theory is more awkward than
| adding them to a set theory like ZFC. One approach to
| universes I've seen in Isabelle/HOL world is to postulate the
| existence of a universe as a model of set theory. But then
| you're stuck reasoning semantically about a model of set
| theory. Nobody has scaled this up to a large pluralist math
| library like Mathlib.
| obeavs wrote:
| So, we've been down this rabbithole at Phosphor (phosphor.co) and
| have explored/made a couple of really big technology bets on it.
|
| The most unique/useful applications of it in production are based
| on combining dependent types with database/graph queries as a
| means. This enables you to take something like RDF which is neat
| in a lot of ways but has a lot of limitations, add typing and
| logic to the queries, in order to generally reimagine how you
| think about querying databases.
|
| For those interested in exploring this space from a "I'd like to
| build something real with this", I'd strongly recommend checking
| out TypeDB (typedb.com). It's been in development for about a
| decade, is faster than MongoDB for vast swaths of things, and is
| one of the most ergonomic frameworks we've found to designing
| complex data applications (Phosphor's core is similar in many
| ways to Palantir's ontology concept). We went into it assuming
| that we were exploring a brand new technology, and have found it
| to work pretty comprehensively for all kinds of production
| settings.
| ubercore wrote:
| Can you expand on
|
| "We build non-dilutive growth engines for industrial and
| climate technology companies by creating high quality
| development pipelines for institutional capital."
| obeavs wrote:
| Sure. Would contextualize by saying that infrastructure is a
| financial product: climate/industrial projects are sited in
| the physical world and have a hard upfront cost to produce a
| long term stream of cash flows, which, from a finance
| perspective, makes it look a lot like debt (e.g. I pay par
| value in order to achieve [x] cash flows with [y] risk).
|
| When you drive past a solar project on the side of the road,
| you see the solar technology producing energy. But in order
| for a bank to fund $100M to construct the project, it has to
| be "developed" as if it were a long-term financial product
| across 15 or so major agreements (power offtake, lease
| agreement, property tax negotiations, etc). The fragmentation
| of tools and context among all the various counterparties
| involved to pull this sort of thing together into a
| creditworthy package for funding is enormously inefficient
| and as a result, processes which should be parallelize-able
| can't be parallelized, creating large amounts of risk into
| the project development process.
|
| While all kinds of asset class-specific tools exist for solar
| or real estate or whatever, most of them are extremely
| limited in function because almost of those things abstract
| down into a narrative that you're communicating to a given
| party at any given time (including your own investment
| committee), and a vast swath of factual information
| represented by deterministic financial calculations and
| hundreds if not thousands of pages of legal documentation.
|
| We build technology to centralize/coordinate/version control
| these workflows in order to unlock an order of magnitude more
| efficiency across that entire process in its totality. But
| instead of selling software, we sell those development +
| financing outcomes (which is where _all_ of the value is in
| this space), because we're actually able to scale that work
| far more effectively than anyone else right now.
| jaggederest wrote:
| Reminds me a lot of AngelList, which was initially
| nominally just a mailing list that connected angels and
| early stage startups, but eventually found that the
| restriction was in special purpose vehicles and automated
| the hard legal work of making many individual funding
| vehicles, and thus was behind the scenes actually a legal
| services company, if you squint.
| Gajurgensen wrote:
| Very interesting. My takeaway is that Dr. Paulson's answer to the
| question is that there is not anything necessarily wrong with
| dependent types, but that he doesn't believe they are necessary.
|
| I would have liked to read more about Lean's alleged performance
| issues, and the issues around intentional equality. For the
| latter, I understand one can run into the need for heterogeneous
| equality (https://lean-lang.org/doc/reference/latest/Basic-
| Proposition...) when types are propositionally equal, but not
| definitionally equal. It has been some time I worked seriously in
| a dependently-typed language, but I recall coming to the
| conclusion that dependent types are best used as little as
| possible, for exactly this reason. If something may be stated as
| a theorem after the fact instead of putting it in the type, that
| was my preference.
|
| Certainly there is something strongly aesthetically appealing
| about dependent type theory. The unification of programs and
| proofs and the natural emergence of independent proof objects. I
| am open to the idea that overly-dogmatic insistence on a type-
| theoretic basis to a theorem prover could lead to pragmatic
| issues, but I'd need to see more examples to be convinced there
| is a better foundation.
|
| Anyway, I agree with Dr. Paulson's point that dependent types
| aren't necessary to verify interesting systems. He talked more of
| pure mathematics, but I am more interested in software
| verification. I work heavily in ACL2 which, not only does it not
| have dependent types, it doesn't have static typing at all! It
| is, however, also a first order logic and the both of these facts
| can sometimes be frustrating. Various libraries have been
| introduced to simulate typing and higher-ordered reasoning.
| hibikir wrote:
| Talking about non-necessary is IMO a cop-out: I bet we can
| verify systems with even fewer features that he is using, or
| just a different set of features that get him to the same spot.
| The interesting question is always whether a feature is useful
| enough.
|
| You get into types at the end. And sure, we don't need static
| types. Just like, outside of verification, we don't need
| garbage collection, or bounds checking, or even loops. But are
| the features useful? What takes us to the goal faster? And
| remember that also changes depending on who is doing the tasks.
| A lot of differents in tooling selection, across all kinds of
| work, come down to preference, not general utility, and they
| sure have nothing to do with necessity
| Gajurgensen wrote:
| I think the question of "necessity" is interesting, because
| between establishing that something is necessary vs the best
| option, I'd say the former is easier. And by agreeing that
| dependent types are not necessary (at least for certain
| design goals) we give space to the folks creating new provers
| to experiment with alternatives, which I think that is a good
| thing. I have been extremely impressed during my limited
| interactions with Lean, but I'm also vaguely aware of enough
| pain points to be interested in what other provers can do
| without being based on curry-howard.
|
| Anyway, for what its worth, I generally agree that static
| typing is preferable. It is just a little more complicated in
| the context of theorem provers (as opposed to general-
| purpose, non-verification programming languages) where, for
| provers not based on type theory, propositions and proof
| obligations can be used where we might otherwise use types.
| This can be nice (generally more flexible, e.g. opportunities
| for non-tagged sums, easy "subtyping"), but also can be a
| downside (sometimes significant work reproducing what you get
| "for free" from a type system).
| zozbot234 wrote:
| The claim that dependently typed languages are inherently reliant
| on fully written-out proof objects looks quite wrong to me. You
| could easily imagine a proof term with opaque typed "holes"
| (written `_`) where the content of each "hole" is simply replaced
| by a LCF-like proof script that was somehow proven (in entirely
| unspecified ways, having to do with the peculiar programming
| language that the LCF-like checker uses for its implementation -
| so the soundness boundary has been expanded a lot, we have given
| up on having an easily checkable 'kernel'!) to generate some term
| of the correct type, starting from its environment. Since the
| content is opaque, no other part of the proof development can
| tell what exactly was in the hole, and we can dispense with
| writing that part of the proof term out.
| whatshisface wrote:
| That doesn't sound that easy.
| zozbot234 wrote:
| If you mean that implementing the LCF architecture OP
| advocates for or evaluating any one implementation of it for
| soundness isn't easy, I absolutely agree. But _assuming_ that
| you 've solved that part, making use of it within a system
| that otherwise uses dependent types is not that hard.
| golemotron wrote:
| The juice isn't worth the squeeze.
| stevan wrote:
| > But people have regularly asked why Isabelle dispenses with
| proof objects. The two questions are essentially the same,
| because proof objects are intrinsic to all the usual type
| theories. They are also completely unnecessary and a huge waste
| of space.
|
| I believe proof by reflection relies on proof objects? Georges
| Gonthier's proof of the four-colour theorem crucially uses proof
| by reflection.
| zozbot234 wrote:
| Proof by reflection is accomplished by running some arbitrary
| program during proof checking that has been proven to only
| return a "true" result if the goal is true. You can do the
| exact same thing in an LCF system, and in fact that's arguably
| what a complex LCF "tactic" amounts to in the first place. If
| anything, the viability of proof by reflection simply shows
| that the divide with LCF-like checkers is not really that
| large.
| heikkilevanto wrote:
| I hate titles like "Why don't you use blah-blah". Usually because
| blah-blah might be an acceptable (maybe good?) solution to a
| problem which I don't have. Let me ask in return: Why should I
| even care about blah-blah. If the first (two?) paragraphs don't
| give a clear answer to that, never mind!
| leegao wrote:
| For what it's worth, the article is the author arguing why they
| don't personally use blah-blah (Dependent Types) despite being
| a leading academic in the field (PLT) where blah-blah is
| frequently touted as the holy grail of that field, and
| justifies his experience using blah-blah-2 (Higher Order
| Logic), a tried and true "sophomoric" choice that seems dusty
| and crusty by comparison (literally, PLT undergrads learn how
| to formalize systems using blah-blah-2-reduced frequently in
| their sophomore years, as a way to learn SML). The rest of the
| article is really only interesting for the PLT/proof automation
| community since it is pretty niche. His conclusions is that you
| don't need the shiny new blah-blah to do things, often in more
| complicated ways, if older blah-blah-2s can do things mostly
| just as well and have the benefit of simplicity and ease of
| automation.
| boulevard wrote:
| The real skill is knowing when not to make something dependent
| otherwise you just slow yourself down.
| tombert wrote:
| My abandoned PhD was in formal methods and I find dependent types
| to be pretty neat, but every time I've tried using a dependently
| typed language for anything it's always been an uphill battle.
|
| When I used to do F# for a living, I was really pushing for using
| F*, but it was impossible to get any buy-in from coworkers
| because the learning curve was comparatively steep. I probably
| should have pushed a bit more, but I figured that I'd potentially
| have more success trying to push people to use TLA+ (though that
| was also unsuccessful).
|
| That was unsuccessful as well, and I've come to the (admittedly
| very cynical conclusion) that software engineers, generally
| speaking, will never learn anything new if it involves "math" in
| any way, shape, or form. Once I realized that, it became much
| easier to lower my expectations of my coworkers.
___________________________________________________________________
(page generated 2025-11-02 23:00 UTC)