[HN Gopher] Some Programming Language Ideas
___________________________________________________________________
Some Programming Language Ideas
Author : toteloader
Score : 97 points
Date : 2025-02-21 15:32 UTC (4 days ago)
(HTM) web link (davidbos.me)
(TXT) w3m dump (davidbos.me)
| tovej wrote:
| Refining a Vecs invariants from program flow is interesting. I'm
| not sure if it's a good thing or not. It hides an interaction
| between references and dynamic container types, possibly
| "protecting" the programmer from understanding the semantics of
| the program.
|
| I also don't see in this particular case why the reference would
| be taken before the potential resizing push but used after the
| push. Maybe with a clearer use-case I could see the point?
|
| This would also introduce dynamic checks at compile time, since
| you need to run the program in order to compile it now, as the
| overload selection/precondition depends on the runtime state of
| the Vec. This necessarily requires a less-strict
| compilation/interpretation mode to be run before the borrow
| checker/other static analysis is done, since the static analysis
| can't know which function is being called. I suppose this is
| similar to compile-time programming.
|
| It strikes me also, that you could do all this at runtime if you
| wanted, simply by manually incrementing length if length < cap
| and assigning to the newly created spot.
| vmchale wrote:
| > Refinement on memory addresses
|
| This is precisely ATS!
| cardanome wrote:
| The endboss of programming languages!
|
| Partly kidding of course, it is a super interesting language.
| It is probably the only language that ever made me feel out
| depth and I dabble in a lot of niche languages. Pretty cool
| stuff!
| kibwen wrote:
| _> In order to guarantee that an addition will not overflow you
| need to check that the integer is below a certain value, for
| example. Or to be sure that indexing an array will not be out of
| bounds you need to check the index value. For this last case Rust
| enables out of bounds access checks for Vecs in debug builds, but
| disables them for release builds._
|
| This is backwards. In Rust, using the indexing operator on an
| array is a bounds-checked operation; the alternative is the
| unsafe .get_unchecked method. This is true regardless of debug
| mode or release mode, and there isn't any flag or configuration
| variable to override this.
|
| It's integer overflow whose behavior (currently) changes between
| debug and release mode, where in debug mode it panics and in
| release mode it's defined to wrap around (and this can be
| configured as you please via a build flag).
| emorning3 wrote:
| If you want to build yet another language then please one that
| solves this problem...
|
| https://en.wikipedia.org/wiki/Expression_problem
|
| This is the problem that makes being a corporate software
| developer really really suck.
| samsquire wrote:
| I agree with you, I perceive it to be really difficult to
| change existing code to fit new things in. There's all
| interactions between things.
|
| The source code of the widgets we use everyday - such as text
| editing or graphical editors are or your web browser's
| Javascript engine, are enormous.
|
| 'Just do X, too' is really difficult with what is already
| there.
| mrkeen wrote:
| Do you have an example of the expression problem that can't
| (yet) be solved in today's programming languages, but could
| theoretically be solved?
| noelwelsh wrote:
| Here you go (not my work, but it's interesting):
| https://github.com/yzyzsun/CP-next
| gavinhoward wrote:
| I solved it in mine. I should write a blog post.
| frabert wrote:
| I once (tried?) to implement some form of refinement types using
| C++17 templates as my BSc thesis: https://github.com/frabert/bsc-
| thesis
|
| It's more or less as horrific as you can imagine...
| pjmlp wrote:
| Nowadays in C++23 land, and with concepts along for the ride,
| it might be easier, although it begs the question why C++ in
| first place?
| weinzierl wrote:
| _" Rust is not a language that has user-definable refinement
| types, but you can find some examples of refinements in the
| standard library, like NonZero and NonNull"_
|
| Rust does not have refinement types but Pattern Types are behind
| a feature flag and will hopefully come soon. Pattern Types are
| not quite refinement types but they will allow you to define
| NonZero et al yourself.
| psd1 wrote:
| I guess F#'s active patterns are refinement types. It's not
| clear to me whether they are types, but they are used like
| types, i.e. "that which matches the specified pattern"
| ratmice wrote:
| This is great, I can't wait to be able to use a NonMax type in
| place of NonZero in a couple of places.
| pmontra wrote:
| About the last part of the post, Ada has asserts if my memory is
| correct. And Oberon, if it's still alive. And Eiffel with
| assertions on preconditions and postconditions of routines
| (functions or procedures.) Probably those features were shared by
| many other languages that were fashionable some 30 years ago and
| never became mainstream. Then Java and C++ did to the industry
| what C did in the 70s/80s and all those features retreated from
| what developers almost used to what researchers wrote in their
| papers.
| pjmlp wrote:
| Java has had such kind of tooling as addon, thing is most folks
| don't care.
|
| https://objectcomputing.com/resources/publications/sett/sept...
|
| C++ contracts might finally land in C++26, after missing two
| revisions, although in a minimal form.
| mrkeen wrote:
| It's because runtime checking is trivial. We can all code up
| something to crash-if-condition, or except-if-condition, or
| log-if-condition.
| Joker_vD wrote:
| We can, yes, but we also can forget to code any such
| condition as well, which is all too common. And for e.g. C
| the lack of an explicitly supplied by the programmer
| runtime-check is exactly equivalent to the programmer
| explicitly stating and pledging that such runtime-check is
| entirely unnecessary, and even it's trivial to statically
| check at compile time that this pledge is in fact false, no
| diagnostics is required.
| imtringued wrote:
| They didn't provide a model checker to accompany the
| contracts the library provides.
|
| No integration with Java Pathfinder or JBMC?
|
| It's really weird how much they missed the ball.
|
| https://en.wikipedia.org/wiki/Java_Pathfinder
|
| https://www.cprover.org/jbmc/
| touisteur wrote:
| Ada has asserts, but also pre/postconditions and contracts,
| invariants, type predicates, not null pointers. Most can be
| checked statically through SPARK ... with some effort.
|
| GNAT also has validity checks, which are very, very useful.
| Fuzzing finds so many bugs with those...
| https://blog.adacore.com/running-american-fuzzy-lop-on-your-...
| jcarrano wrote:
| I was trying something in the line of refinement types in C++ to
| solve the sequential method (anti)pattern, without success. For
| example, one would have
|
| ConfiguredThing Thing::configure(....) &&;
|
| Where ConfiguredThing and Thing have the exact same members, so
| doing
|
| auto y = std::move(x).configure(...);
|
| would not copy any data around. It seemed to work with
| optimizations on, but then there are no guarantees that it will
| always be the case.
|
| Ideally one would want RAII, but that is not always possible, in
| particular when wrapping C libraries that may have their own
| logic. Also, the object could be in different states, with
| different methods available in each state, and then it would be
| possible to prevent errors at compile time.
| jcarrano wrote:
| On a second thought, this may be more in the direction of
| linear types.
| pjmlp wrote:
| Some of the ideas are present in other languages beyond those
| described.
|
| Many do type flow analysis nowadays.
|
| Variant records in Wirthian languages are another approach,
| although they lack validation regarding accessing wrong active
| tags.
|
| Ada/SPARK and Frama-C can do refinement on memory addresses.
| christianqchung wrote:
| The last section, "Checked bending of the rules" seems pretty
| similar to C++ contracts[0], though the behavior on violations
| looks like it will be able to vary wildly between consteval and
| regular contexts, and whether it terminates the running program
| with a contract violation handler.
|
| [0] https://en.cppreference.com/w/cpp/language/contracts
| virtualritz wrote:
| For refinement types in Rust see e.g.:
|
| https://crates.io/crates/refined_type
|
| https://crates.io/crates/refinement
|
| and
|
| https://crates.io/crates/refined
|
| There are also some interesting optimizations possible around
| this; see e.g. this discussion on the issue tracker of the latter
| crate:
| https://github.com/jkaye2012/refined/issues/9#issuecomment-2...
___________________________________________________________________
(page generated 2025-02-25 23:02 UTC)