!TZcOjRPmzyRVIRZDcf:matrix.org

Pikelet

56 Members
+pikelet:matrix.org - github.com/pikelet-lang - General discussion about Pikelet, a dependently typed programming language7 Servers

Load older messages


SenderMessageTime
16 May 2021
@_discord_280132690059984897:t2bot.iobrendanzab I kind of don't want to push myself to think too hard about that yet though 😅 04:06:33
@_discord_535117309732323328:t2bot.ioBoarders Yeah, I got completely overwhelmed when I wanted to try to actually compile to native code and decided at that point that I would stick with targetting specific backends as that is more my flavour 04:07:24
@_discord_280132690059984897:t2bot.iobrendanzab yeah 04:07:32
@_discord_280132690059984897:t2bot.iobrendanzab I think it's easy to overwhelm yourself if you try to think about too much stuff 04:07:58
@_discord_535117309732323328:t2bot.ioBoarders Suddenly I am reading papers about GC and immutable beans and regions and CPS vs ANF and ahhh 04:08:03
@_discord_280132690059984897:t2bot.iobrendanzab hahh that's a mood 04:08:15
@_discord_535117309732323328:t2bot.ioBoarders * Suddenly I am reading papers about GC and immutable beans and regions and CPS vs ANF and ahhh 04:08:17
@_discord_535117309732323328:t2bot.ioBoarders What is the idea with the Fathom language? I'm afraid to say I am too ignorant to immediately grasp what a language for formally specifying binary formats means. 04:16:48
@_discord_280132690059984897:t2bot.iobrendanzab ahhh - so yeah say for a format file like OpenType, the specification of the binary format is done as a bunch of english prose 04:17:49
@_discord_280132690059984897:t2bot.iobrendanzab telling you what bytes to expect where 04:18:18
@_discord_280132690059984897:t2bot.iobrendanzab so you might read a number, than that's assumed ahead of time to tell you the number of items to expect next 04:18:59
@_discord_280132690059984897:t2bot.iobrendanzab so based on that data you then know format of upcoming data 04:19:26
@_discord_280132690059984897:t2bot.iobrendanzab so you have some sort of data dependency there 04:19:41
@_discord_535117309732323328:t2bot.ioBoarders Ah ok, I see 04:19:46
@_discord_280132690059984897:t2bot.iobrendanzab and this stuff can get pretty complicated 04:19:53
@_discord_280132690059984897:t2bot.iobrendanzab * and this stuff can get pretty complicated 04:19:54
@_discord_535117309732323328:t2bot.ioBoarders That is very cool stuff 04:19:54
@_discord_535117309732323328:t2bot.ioBoarders Sounds like it should connect up with works on fuzzers quite nicely 04:20:09
@_discord_280132690059984897:t2bot.iobrendanzab so you want to make sure you're taking into account integer bounds etc. in you specification and saying what people should do in those cases 04:20:46
@_discord_535117309732323328:t2bot.ioBoarders Though I guess if you have a type checker for meeting the binary specification then a fuzzer would need a type unchecker 04:20:49
@_discord_280132690059984897:t2bot.iobrendanzab hehe 04:20:53
@_discord_280132690059984897:t2bot.iobrendanzab so yeah, Fathom is like a dependently typed language with a built-in universe of format descriptions 04:21:34
@_discord_535117309732323328:t2bot.ioBoarders Amazing, I love to hear these kind of usages 04:21:53
@_discord_280132690059984897:t2bot.iobrendanzab and it compiles those format descriptions to parsers and pretty printers 04:22:12
@_discord_280132690059984897:t2bot.iobrendanzab at least, it should do, once I figure out all the stuff 😔 04:22:32
@_discord_535117309732323328:t2bot.ioBoarders ah yeah, great stuff 04:22:47
@_discord_280132690059984897:t2bot.iobrendanzab like ideally Fathom is something that could just be embedded in a dependently typed language 04:25:25
@_discord_280132690059984897:t2bot.iobrendanzab but most dependently typed languages are really bad for compiling to native code, caring about memory layout, staging, etc. 04:26:10
@_discord_280132690059984897:t2bot.iobrendanzab unless you do the translation manually and do all the proofs 04:26:42
@_discord_280132690059984897:t2bot.iobrendanzab plus the toolchains and UX of using provers is a pain - I want something that can plug into a tool like cargo pretty nicely 04:27:26

There are no newer messages yet.


Back to Room List